1  /-
  2  Copyright (c) 2015, 2017 Jeremy Avigad. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel
  5  -/
  6  
  7  import data.real.nnreal data.real.ennreal
src         └──────────────┘ └───────────────┘
  8  import topology.uniform_space.separation topology.uniform_space.uniform_embedding topology.uniform_space.pi
src         └───────────────────────────────┘ └──────────────────────────────────────┘ └───────────────────────┘
  9  import topology.bases
src         └────────────┘
 10  
 11  /-!
 12  # Extended metric spaces
 13  
 14  This file is devoted to the definition and study of `emetric_spaces`, i.e., metric
 15  spaces in which the distance is allowed to take the value ∞. This extended distance is
 16  called `edist`, and takes values in `ennreal`.
 17  
 18  Many definitions and theorems expected on emetric spaces are already introduced on uniform spaces and
 19  topological spaces. For example:
 20    open and closed sets, compactness, completeness, continuity and uniform continuity
 21  
 22  The class `emetric_space` therefore extends `uniform_space` (and `topological_space`).
 23  -/
 24  
 25  open lattice set filter classical
 26  noncomputable theory
 27  
 28  open_locale uniformity topological_space
 29  
 30  universes u v w
 31  variables {α : Type u} {β : Type v} {γ : Type w}
 32  
 33  /-- Characterizing uniformities associated to a (generalized) distance function `D`
 34  in terms of the elements of the uniformity. -/
 35  theorem uniformity_dist_of_mem_uniformity [linear_order β] {U : filter (α × α)} (z : β) (D : α → α → β)
id                                              └──────────┘        └────┘                         
src                                             └──────────┘         └────┘    
typ                                             └──────────┘        └────┘                         
 36    (H : ∀ s, s ∈ U ↔ ∃ε>z, ∀{a b:α}, D a b < ε → (a, b) ∈ s) :
id                                         
src                                                   
typ                                        
 37    U = ⨅ ε>z, principal {p:α×α | D p.1 p.2 < ε} :=
id          └───────┘            
src            └───────┘                
typ         └───────┘            
doc             └───────┘
 38  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
 39    (le_infi $ λ ε, le_infi $ λ ε0, le_principal_iff.2 $ (H _).2 ⟨ε, ε0, λ a b, id⟩)
id      └─────┘       └─────┘     └┘  └──────────────┘             └┘       └┘
src     └─────┘        └─────┘         └──────────────┘                          └┘
typ     └─────┘       └─────┘     └┘  └──────────────┘             └┘       └┘
 40    (λ r ur, let ⟨ε, ε0, h⟩ := (H _).1 ur in
id         └┘  └─┘    └┘             └┘
src                                    
typ        └┘  └─┘    └┘             └┘
 41      mem_infi_sets ε $ mem_infi_sets ε0 $ mem_principal_sets.2 $ λ ⟨a, b⟩, h)
id       └───────────┘     └───────────┘      └────────────────┘      
src      └───────────┘     └───────────┘      └────────────────┘
typ      └───────────┘     └───────────┘      └────────────────┘      
 42  
 43  class has_edist (α : Type*) := (edist : α → α → ennreal)
id                        └───┘                   └─────┘
src                                                  └─────┘
typ                       └───┘                   └─────┘
doc                                                  └─────┘
 44  export has_edist (edist)
 45  
 46  /- Design note: one could define an `emetric_space` just by giving `edist`, and then
 47  derive an instance of `uniform_space` by taking the natural uniform structure
 48  associated to the distance. This creates diamonds problem for products, as the
 49  uniform structure on the product of two emetric spaces could be obtained first
 50  by obtaining two uniform spaces and then taking their products, or by taking
 51  the product of the emetric spaces and then the associated uniform structure.
 52  The two uniform structure we have just described are equal, but not defeq, which
 53  creates a lot of problem.
 54  
 55  The idea is to add, in the very definition of an `emetric_space`, a uniform structure
 56  with a uniformity which equal to the one given by the distance, but maybe not defeq.
 57  And the instance from `emetric_space` to `uniform_space` uses this uniformity.
 58  In this way, when we create the product of emetric spaces, we put in the product
 59  the uniformity corresponding to the product of the uniformities. There is one more
 60  proof obligation, that this product uniformity is equal to the uniformity corresponding
 61  to the product metric. But the diamond problem disappears.
 62  
 63  The same trick is used in the definition of a metric space, where one stores as well
 64  a uniform structure and an edistance. -/
 65  
 66  /-- Creating a uniform space from an extended distance. -/
 67  def uniform_space_of_edist
 68    (edist : α → α → ennreal)
 69    (edist_self : ∀ x : α, edist x x = 0)
 70    (edist_comm : ∀ x y : α, edist x y = edist y x)
 71    (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z) : uniform_space α :=
 72  uniform_space.of_core {
 73    uniformity := (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}),
 74    refl       := le_infi $ assume ε, le_infi $
 75      by simp [set.subset_def, id_rel, edist_self, (>)] {contextual := tt},
id                                                                        └┘
src         └────┘              └┘      └┘          └┘ └──┘ └────────────┘└┘
typ         └────┘              └┘      └┘          └┘ └──┘ └────────────┘└┘
doc         └────┘              └┘      └┘          └┘ └──┘ └────────────┘  
txt         └────┘              └┘      └┘          └┘ └──┘ └────────────┘  
par         └────┘              └┘      └┘          └┘ └──┘ └────────────┘  
pid                           └┘      └┘          └┘ └─┘ └────────────┘  
st                                                               └──────────┘
 76    comp       :=
 77      le_infi $ assume ε, le_infi $ assume h,
id       └─────┘            └─────┘          
src      └─────┘             └─────┘
typ      └─────┘            └─────┘          
 78      have (2 : ennreal) = (2 : ℕ) := by simp,
id                 └─────┘        
src                └─────┘                └──┘
typ                └─────┘                └──┘
doc                └─────┘                  └──┘
txt                                         └──┘
par                                         └──┘
st                                         └───┘
 79      have A : 0 < ε / 2 := ennreal.div_pos_iff.2 ⟨ne_of_gt h, this ▸ ennreal.nat_ne_top 2⟩,
id                          └─────────────────┘   └──────┘   └──┘  └────────────────┘
src                          └─────────────────┘   └──────┘          └────────────────┘
typ                         └─────────────────┘   └──────┘   └──┘  └────────────────┘
 80      lift'_le
id       └──────┘
src      └──────┘
typ      └──────┘
 81      (mem_infi_sets (ε / 2) $ mem_infi_sets A (subset.refl _)) $
id        └───────────┘         └───────────┘   └─────────┘
src       └───────────┘          └───────────┘    └─────────┘
typ       └───────────┘         └───────────┘   └─────────┘
 82      have ∀ (a b c : α), edist a c < ε / 2 → edist c b < ε / 2 → edist a b < ε,
id                          └───┘          └───┘          └───┘    
src                                                                        
typ                         └───┘          └───┘          └───┘    
 83        from assume a b c hac hcb,
id                        └─┘ └─┘
typ                       └─┘ └─┘
 84        calc edist a b ≤ edist a c + edist c b : edist_triangle _ _ _
id              └───┘     └───┘    └───┘     └────────────┘
src                                   
typ             └───┘     └───┘    └───┘     └────────────┘
 85          ... < ε / 2 + ε / 2 : ennreal.add_lt_add hac hcb
id                            └────────────────┘ └─┘ └─┘
src                             └────────────────┘
typ                           └────────────────┘ └─┘ └─┘
 86          ... = ε : by rw [ennreal.add_halves],
id                           └────────────────┘
src                       └──┘└────────────────┘
typ                      └──┘└────────────────┘
doc                       └──┘                  
txt                       └──┘                  
par                       └──┘                  
pid                         └┘                  
st                       └─────────────────────┘
 87      by simpa [comp_rel],
id                 └──────┘
src         └─────┘└──────┘
typ         └─────┘└──────┘
doc         └─────┘└──────┘
txt         └─────┘        
par         └─────┘        
pid                      
st         └───────────────┘
 88    symm       := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
id                   └──────────┘             └──────────┘           
src                  └──────────┘              └──────────┘
typ                  └──────────┘             └──────────┘           
 89      tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ by simp [edist_comm] }
id       └───────────┘    └───────────┘    └─────────────────────────┘             └────────┘
src      └───────────┘     └───────────┘     └─────────────────────────┘       └────┘          └┘
typ      └───────────┘    └───────────┘    └─────────────────────────┘       └────┘└────────┘└┘
doc                                                                             └────┘          └┘
txt                                                                             └────┘          └┘
par                                                                             └────┘          └┘
pid                                                                                           
st                                                                             └─────────────────┘
 90  
 91  section prio
 92  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
 93  /-- Extended metric spaces, with an extended distance `edist` possibly taking the
 94  value ∞
 95  
 96  Each emetric space induces a canonical `uniform_space` and hence a canonical `topological_space`.
 97  This is enforced in the type class definition, by extending the `uniform_space` structure. When
 98  instantiating an `emetric_space` structure, the uniformity fields are not necessary, they will be
 99  filled in by default. There is a default value for the uniformity, that can be substituted
100  in cases of interest, for instance when instantiating an `emetric_space` structure
101  on a product.
102  
103  Continuity of `edist` is finally proving in `topology.instances.ennreal`
104  -/
105  class emetric_space (α : Type u) extends has_edist α : Type u :=
id                            └──┘            └───────┘ 
src                                           └───────┘
typ                           └──┘            └───────┘ 
106  (edist_self : ∀ x : α, edist x x = 0)
id                        └───┘   
src                                   
typ                       └───┘   
107  (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y)
id                                     └───┘          
src                                                       
typ                                    └───┘          
108  (edist_comm : ∀ x y : α, edist x y = edist y x)
id                          └───┘    └───┘  
src                                     
typ                         └───┘    └───┘  
109  (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z)
id                                └───┘    └───┘    └───┘  
src                                                      
typ                               └───┘    └───┘    └───┘  
110  (to_uniform_space : uniform_space α := uniform_space_of_edist edist edist_self edist_comm edist_triangle)
id                       └───────────┘     └────────────────────┘ └───┘ └────────┘ └────────┘ └────────────┘
src                      └───────────┘      └────────────────────┘
typ                      └───────────┘     └────────────────────┘ └───┘ └────────┘ └────────┘ └────────────┘
doc                      └───────────┘      └────────────────────┘
111  (uniformity_edist : 𝓤 α = ⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε} . control_laws_tac)
id                              └───────┘      └───┘      
src                               └───────┘                    
typ                             └───────┘      └───┘      
doc                               └───────┘
112  end prio
113  
114  /- emetric spaces are less common than metric spaces. Therefore, we work in a dedicated
115  namespace, while notions associated to metric spaces are mostly in the root namespace. -/
116  variables [emetric_space α]
id              └───────────┘
src             └───────────┘
typ             └───────────┘
doc             └───────────┘
117  
118  @[priority 100] -- see Note [lower instance priority]
119  instance emetric_space.to_uniform_space' : uniform_space α :=
id                                              └───────────┘ 
src                                             └───────────┘
typ                                             └───────────┘ 
doc                                             └───────────┘
120  emetric_space.to_uniform_space α
id   └────────────────────────────┘ 
src  └────────────────────────────┘
typ  └────────────────────────────┘ 
121  
122  export emetric_space (edist_self eq_of_edist_eq_zero edist_comm edist_triangle)
123  
124  attribute [simp] edist_self
id                    └────────┘
src                   └────────┘
typ                   └────────┘
doc             └──┘
125  
126  /-- Characterize the equality of points by the vanishing of their extended distance -/
127  @[simp] theorem edist_eq_zero {x y : α} : edist x y = 0 ↔ x = y :=
id                                            └───┘         
src                                            └───┘           
typ                                           └───┘         
doc    └──┘
128  iff.intro eq_of_edist_eq_zero (assume : x = y, this ▸ edist_self _)
id   └───────┘ └─────────────────┘               └──┘  └────────┘
src  └───────┘ └─────────────────┘                       └────────┘
typ  └───────┘ └─────────────────┘               └──┘  └────────┘
129  
130  @[simp] theorem zero_eq_edist {x y : α} : 0 = edist x y ↔ x = y :=
id                                               └───┘      
src                                               └───┘        
typ                                              └───┘      
doc    └──┘
131  iff.intro (assume h, eq_of_edist_eq_zero (h.symm))
id   └───────┘           └─────────────────┘  └───┘
src  └───────┘            └─────────────────┘   └───┘
typ  └───────┘           └─────────────────┘  └───┘
132            (assume : x = y, this ▸ (edist_self _).symm)
id                           └──┘   └────────┘   └──┘
src                                   └────────┘   └──┘
typ                          └──┘   └────────┘   └──┘
133  
134  theorem edist_le_zero {x y : α} : (edist x y ≤ 0) ↔ x = y :=
id                                     └───┘          
src                                     └───┘            
typ                                    └───┘          
135  le_zero_iff_eq.trans edist_eq_zero
id   └────────────┘└────┘ └───────────┘
src  └────────────┘└────┘ └───────────┘
typ  └────────────┘└────┘ └───────────┘
doc                       └───────────┘
136  
137  /-- Triangle inequality for the extended distance -/
138  theorem edist_triangle_left (x y z : α) : edist x y ≤ edist z x + edist z y :=
id                                            └───┘    └───┘    └───┘  
src                                            └───┘      └───┘      └───┘
typ                                           └───┘    └───┘    └───┘  
139  by rw edist_comm z; apply edist_triangle
id         └────────┘         └────────────┘
src     └─┘└────────┘   └────┘└────────────┘
typ     └─┘└────────┘  └────┘└────────────┘
doc     └─┘             └────┘              
txt     └─┘             └────┘              
par     └─┘             └────┘              
pid                                       
st     └──────────────────────────────────────
140  
src  
typ  
doc  
txt  
par  
pid  
st   
141  theorem edist_triangle_right (x y z : α) : edist x y ≤ edist x z + edist y z :=
id                                             └───┘    └───┘    └───┘  
src                                             └───┘      └───┘      └───┘
typ                                            └───┘    └───┘    └───┘  
142  by rw edist_comm y; apply edist_triangle
id         └────────┘         └────────────┘
src     └─┘└────────┘   └────┘└────────────┘
typ     └─┘└────────┘  └────┘└────────────┘
doc     └─┘             └────┘              
txt     └─┘             └────┘              
par     └─┘             └────┘              
pid                                       
st     └──────────────────────────────────────
143  
src  
typ  
doc  
txt  
par  
pid  
st   
144  lemma edist_triangle4 (x y z t : α) :
id                                    
typ                                   
145    edist x t ≤ edist x y + edist y z + edist z t :=
id     └───┘    └───┘    └───┘    └───┘  
src    └───┘      └───┘      └───┘      └───┘
typ    └───┘    └───┘    └───┘    └───┘  
146  calc
147    edist x t ≤ edist x z + edist z t : edist_triangle x z t
id     └───┘     └───┘    └───┘     └────────────┘   
src    └───┘       └───┘      └───┘       └────────────┘
typ    └───┘     └───┘    └───┘     └────────────┘   
148  ... ≤ (edist x y + edist y z) + edist z t : add_le_add_right' (edist_triangle x y z)
id          └───┘    └───┘     └───┘     └───────────────┘  └────────────┘   
src         └───┘      └───┘       └───┘       └───────────────┘  └────────────┘
typ         └───┘    └───┘     └───┘     └───────────────┘  └────────────┘   
149  
150  /-- The triangle (polygon) inequality for sequences of points; `finset.Ico` version. -/
151  lemma edist_le_Ico_sum_edist (f : ℕ → α) {m n} (h : m ≤ n) :
id                                                       
src                                                       
typ                                                      
152    edist (f m) (f n) ≤ (finset.Ico m n).sum (λ i, edist (f i) (f (i + 1))) :=
id     └───┘           └────────┘   └─┘       └───┘         
src    └───┘               └────────┘     └─┘        └───┘             
typ    └───┘           └────────┘   └─┘       └───┘         
doc                         └────────┘
153  begin
st   └─────
154    revert n,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          └┘
st   ─────────┘└─
155    refine nat.le_induction _ _,
id            └──────────────┘
src    └─────┘└──────────────┘└──┘
typ    └─────┘└──────────────┘└──┘
doc    └─────┘└──────────────┘└──┘
txt    └─────┘                └──┘
par    └─────┘                └──┘
pid                          └──┘
st   ────────────────────────────┘└─
156    { simp only [finset.sum_empty, finset.Ico.self_eq_empty, edist_self],
id                  └──────────────┘  └──────────────────────┘  └────────┘
src      └─────────┘└──────────────┘└┘└──────────────────────┘└┘└────────┘
typ      └─────────┘└──────────────┘└┘└──────────────────────┘└┘└────────┘
doc      └─────────┘                └┘                        └┘          
txt      └─────────┘                └┘                        └┘          
par      └─────────┘                └┘                        └┘          
pid          └──┘└┘                └┘                        └┘          
st   ───┘└────────────────────────────────────────────────────────────────┘└─
157      -- TODO: Why doesn't Lean close this goal automatically? `apply le_refl` fails too.
st   ────────────────────────────────────────────────────────────────────────────────────────
158      exact le_refl (0:ennreal) },
id             └─────┘    └─────┘
src      └────┘└─────┘ └┘└─────┘└┘
typ      └────┘└─────┘ └┘└─────┘└┘
doc      └────┘        └┘└─────┘└┘
txt      └────┘        └┘       └┘
par      └────┘        └┘       └┘
pid                   └┘       
st   ─────────────────────────────┘└┘
159    { assume n hn hrec,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid      └──────────────┘
st   ───────────────────┘└─
160      calc edist (f m) (f (n+1)) ≤ edist (f m) (f n) + edist (f n) (f (n+1)) : edist_triangle _ _ _
id       └──┘                                           └───┘                 └────────────┘
src      └──┘                                            └───┘                   └────────────┘
typ      └──┘                                           └───┘                 └────────────┘
doc      └──┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
161        ... ≤ (finset.Ico m n).sum _ + _ : add_le_add' hrec (le_refl _)
id                               └─┘          └─────────┘ └──┘  └─────┘
src                              └─┘          └─────────┘       └─────┘
typ                              └─┘          └─────────┘ └──┘  └─────┘
st   ──────────────────────────────────────────────────────────────────────
162        ... = (finset.Ico m (n+1)).sum _ :
id                └────────┘         └─┘
src               └────────┘         └─┘
typ               └────────┘         └─┘
doc               └────────┘
st   ─────────────────────────────────────────
163          by rw [finset.Ico.succ_top hn, finset.sum_insert, add_comm]; simp }
id                  └─────────────────┘ └┘  └───────────────┘  └──────┘
src             └──┘└─────────────────┘  └┘└───────────────┘└┘└──────┘  └───┘
typ             └──┘└─────────────────┘└┘└┘└───────────────┘└┘└──────┘  └───┘
doc             └──┘                     └┘                 └┘          └───┘
txt             └──┘                     └┘                 └┘          └───┘
par             └──┘                     └┘                 └┘          └───┘
pid               └┘                     └┘                 └┘              
st   ─────────┘└─────────────────────────┘└─────────────────┘└────────┘└─────┘└─
164  end
st   ──┘
165  
166  /-- The triangle (polygon) inequality for sequences of points; `finset.range` version. -/
167  lemma edist_le_range_sum_edist (f : ℕ → α) (n : ℕ) :
id                                                 
src                                                 
typ                                                
168    edist (f 0) (f n) ≤ (finset.range n).sum (λ i, edist (f i) (f (i + 1))) :=
id     └───┘            └──────────┘  └─┘       └───┘         
src    └───┘               └──────────┘   └─┘        └───┘             
typ    └───┘            └──────────┘  └─┘       └───┘         
doc                         └──────────┘
169  finset.Ico.zero_bot n ▸ edist_le_Ico_sum_edist f (nat.zero_le n)
id   └─────────────────┘   └────────────────────┘   └─────────┘ 
src  └─────────────────┘    └────────────────────┘    └─────────┘
typ  └─────────────────┘   └────────────────────┘   └─────────┘ 
doc                          └────────────────────┘
170  
171  /-- A version of `edist_le_Ico_sum_edist` with each intermediate distance replaced
172  with an upper estimate. -/
173  lemma edist_le_Ico_sum_of_edist_le {f : ℕ → α} {m n} (hmn : m ≤ n)
id                                                               
src                                                               
typ                                                              
174    {d : ℕ → ennreal} (hd : ∀ {k}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) :
id             └─────┘                        └───┘                
src            └─────┘                             └───┘                  
typ            └─────┘                        └───┘                
doc             └─────┘
175    edist (f m) (f n) ≤ (finset.Ico m n).sum d :=
id     └───┘           └────────┘   └─┘  
src    └───┘               └────────┘     └─┘
typ    └───┘           └────────┘   └─┘  
doc                         └────────┘
176  le_trans (edist_le_Ico_sum_edist f hmn) $
id   └──────┘  └────────────────────┘  └─┘
src  └──────┘  └────────────────────┘
typ  └──────┘  └────────────────────┘  └─┘
doc            └────────────────────┘
177  finset.sum_le_sum $ λ k hk, hd (finset.Ico.mem.1 hk).1 (finset.Ico.mem.1 hk).2
id   └───────────────┘      └┘  └┘  └────────────┘  └┘    └────────────┘  └┘ 
src  └───────────────┘               └────────────┘        └────────────┘     
typ  └───────────────┘      └┘  └┘  └────────────┘  └┘    └────────────┘  └┘ 
178  
179  /-- A version of `edist_le_range_sum_edist` with each intermediate distance replaced
180  with an upper estimate. -/
181  lemma edist_le_range_sum_of_edist_le {f : ℕ → α} (n : ℕ)
id                                                       
src                                                       
typ                                                      
182    {d : ℕ → ennreal} (hd : ∀ {k}, k < n → edist (f k) (f (k + 1)) ≤ d k) :
id             └─────┘                   └───┘                
src            └─────┘                      └───┘                  
typ            └─────┘                   └───┘                
doc             └─────┘
183    edist (f 0) (f n) ≤ (finset.range n).sum d :=
id     └───┘            └──────────┘  └─┘  
src    └───┘               └──────────┘   └─┘
typ    └───┘            └──────────┘  └─┘  
doc                         └──────────┘
184  finset.Ico.zero_bot n ▸ edist_le_Ico_sum_of_edist_le (zero_le n) (λ _ _, hd)
id   └─────────────────┘   └──────────────────────────┘  └─────┘         └┘
src  └─────────────────┘    └──────────────────────────┘  └─────┘
typ  └─────────────────┘   └──────────────────────────┘  └─────┘         └┘
doc                          └──────────────────────────┘
185  
186  /-- Two points coincide if their distance is `< ε` for all positive ε -/
187  theorem eq_of_forall_edist_le {x y : α} (h : ∀ε, ε > 0 → edist x y ≤ ε) : x = y :=
id                                                        └───┘          
src                                                          └───┘             
typ                                                       └───┘          
188  eq_of_edist_eq_zero (eq_of_le_of_forall_le_of_dense bot_le h)
id   └─────────────────┘  └────────────────────────────┘ └────┘ 
src  └─────────────────┘  └────────────────────────────┘ └────┘
typ  └─────────────────┘  └────────────────────────────┘ └────┘ 
189  
190  /-- Reformulation of the uniform structure in terms of the extended distance -/
191  theorem uniformity_edist' : 𝓤 α = (⨅ ε>0, principal {p:α×α | edist p.1 p.2 < ε}) :=
id                                       └───────┘      └───┘      
src                                        └───────┘        └───┘       
typ                                      └───────┘      └───┘      
doc                                         └───────┘
192  emetric_space.uniformity_edist _
id   └────────────────────────────┘
src  └────────────────────────────┘
typ  └────────────────────────────┘
193  
194  /-- Reformulation of the uniform structure in terms of the extended distance on a subtype -/
195  theorem uniformity_edist'' : 𝓤 α = (⨅ε:{ε:ennreal // ε>0}, principal {p:α×α | edist p.1 p.2 < ε.val}) :=
id                                        └─────┘       └───────┘      └───┘      └──┘
src                                        └─────┘        └───────┘        └───┘         └──┘
typ                                       └─────┘       └───────┘      └───┘      └──┘
doc                                          └─────┘         └───────┘
196  by { simp only [infi_subtype], exact uniformity_edist' }
id                   └──────────┘         └───────────────┘
src       └─────────┘└──────────┘  └────┘└───────────────┘
typ       └─────────┘└──────────┘  └────┘└───────────────┘
doc       └─────────┘              └────┘└───────────────┘
txt       └─────────┘              └────┘                 
par       └─────────┘              └────┘                 
pid           └──┘└┘                                    
st     └─────────────────────────┘└────────────────────────┘└┘
197  
198  /-- Characterization of the elements of the uniformity in terms of the extended distance -/
199  theorem mem_uniformity_edist {s : set (α×α)} :
id                                     └─┘  
src                                    └─┘   
typ                                    └─┘  
200    s ∈ 𝓤 α ↔ (∃ε>0, ∀{a b:α}, edist a b < ε → (a, b) ∈ s) :=
id                       └───┘            
src                          └───┘                
typ                      └───┘            
doc        
201  begin
st   └─────
202    rw [uniformity_edist'', mem_infi],
id         └────────────────┘  └──────┘
src    └──┘└────────────────┘└┘└──────┘
typ    └──┘└────────────────┘└┘└──────┘
doc    └──┘└────────────────┘└┘        
txt    └──┘                  └┘        
par    └──┘                  └┘        
pid      └┘                  └┘        
st   ───────────────────────┘└────────┘└──
203    simp [subset_def],
id           └────────┘
src    └────┘└────────┘
typ    └────┘└────────┘
doc    └────┘          
txt    └────┘          
par    └────┘          
pid                  
st   ──────────────────┘└─
204    exact assume ⟨r, hr⟩ ⟨p, hp⟩, ⟨⟨min r p, lt_min hr hp⟩, by simp [lt_min_iff, (≥)] {contextual := tt}⟩,
id                     └┘     └┘     └─┘      └────┘                  └────────┘                     └┘
src    └────┘      └┘ └┘  └─┘ └┘  └─┘  └─┘  └┘└────┘    └─┘  └────┘└────────┘└┘└──┘ └────────────┘└┘
typ    └────┘      └┘└┘└┘└─┘└┘└┘└─┘  └─┘  └┘└────┘    └─┘  └────┘└────────┘└┘└──┘ └────────────┘└┘
doc    └────┘      └┘ └┘  └─┘ └┘  └─┘       └┘          └─┘  └────┘          └┘ └──┘ └────────────┘  
txt    └────┘      └┘ └┘  └─┘ └┘  └─┘       └┘          └─┘  └────┘          └┘ └──┘ └────────────┘  
par    └────┘      └┘ └┘  └─┘ └┘  └─┘       └┘          └─┘  └────┘          └┘ └──┘ └────────────┘  
pid               └┘ └┘  └─┘ └┘  └─┘       └┘          └─┘  └─────┘          └┘ └──┘ └────────────┘  └┘
st   ───────────────────────────────────────────────────────────┘└────────────────────────────────────────┘└─
205    exact ⟨⟨1, ennreal.zero_lt_one⟩⟩
id                └─────────────────┘
src    └────┘  └─┘└─────────────────┘└─┘
typ    └────┘  └─┘└─────────────────┘└─┘
doc    └────┘  └─┘                   └─┘
txt    └────┘  └─┘                   └─┘
par    └────┘  └─┘                   └─┘
pid           └─┘                   └┘
st   ──────────────────────────────────┘
206  end
st   └─┘
207  
208  /-- Fixed size neighborhoods of the diagonal belong to the uniform structure -/
209  theorem edist_mem_uniformity {ε:ennreal} (ε0 : 0 < ε) :
id                                   └─────┘           
src                                  └─────┘          
typ                                  └─────┘           
doc                                  └─────┘
210    {p:α×α | edist p.1 p.2 < ε} ∈ 𝓤 α :=
id          └───┘          
src           └───┘            
typ         └───┘          
doc                                  
211  mem_uniformity_edist.2 ⟨ε, ε0, λ a b, id⟩
id   └──────────────────┘     └┘       └┘
src  └──────────────────┘                 └┘
typ  └──────────────────┘     └┘       └┘
doc  └──────────────────┘
212  
213  theorem uniformity_edist_nnreal :
214    𝓤 α = (⨅(ε:nnreal) (h : ε > 0), principal {p:α×α | edist p.1 p.2 < ε}) :=
id            └────┘            └───────┘      └───┘      
src            └────┘             └───────┘        └───┘       
typ           └────┘            └───────┘      └───┘      
doc             └────┘              └───────┘
215  begin
st   └─────
216    rw [uniformity_edist', ennreal.infi_ennreal, inf_of_le_left],
id         └───────────────┘  └──────────────────┘  └────────────┘
src    └──┘└───────────────┘└┘└──────────────────┘└┘└────────────┘
typ    └──┘└───────────────┘└┘└──────────────────┘└┘└────────────┘
doc    └──┘└───────────────┘└┘                    └┘              
txt    └──┘                 └┘                    └┘              
par    └──┘                 └┘                    └┘              
pid      └┘                 └┘                    └┘              
st   ──────────────────────┘└────────────────────┘└──────────────┘└──
217    { congr, funext ε, refine infi_congr_Prop ennreal.coe_pos _, assume h, refl },
id                               └─────────────┘ └─────────────┘
src      └───┘  └──────┘  └─────┘└─────────────┘└─────────────┘└┘  └──────┘  └───┘
typ      └───┘  └──────┘  └─────┘└─────────────┘└─────────────┘└┘  └──────┘  └───┘
doc             └──────┘  └─────┘                              └┘  └──────┘  └───┘
txt      └───┘  └──────┘  └─────┘                              └┘  └──────┘  └───┘
par      └───┘  └──────┘  └─────┘                              └┘  └──────┘  └───┘
pid                   └┘                                      └┘  └──────┘      
st   ───┘└───┘└────────┘└────────────────────────────────────────┘└────────┘└─────┘└┘
218    refine le_infi (assume h, infi_le_of_le 1 $ infi_le_of_le ennreal.zero_lt_one $ _),
id            └─────┘                              └───────────┘ └─────────────────┘
src    └─────┘└─────┘       └──┘             └─┘ └───────────┘└─────────────────┘ └─┘
typ    └─────┘└─────┘       └──┘             └─┘ └───────────┘└─────────────────┘ └─┘
doc    └─────┘              └──┘             └─┘                                  └─┘
txt    └─────┘              └──┘             └─┘                                  └─┘
par    └─────┘              └──┘             └─┘                                  └─┘
pid                        └──┘             └─┘                                  └─┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
219    exact principal_mono.2 (assume p h, lt_of_lt_of_le h le_top)
id           └────────────┘                └────────────┘   └────┘
src    └────┘└────────────┘└─┘       └────┘└────────────┘ └────┘└┘
typ    └────┘└────────────┘└─┘       └────┘└────────────┘ └────┘└┘
doc    └────┘              └─┘       └────┘                     └┘
txt    └────┘              └─┘       └────┘                     └┘
par    └────┘              └─┘       └────┘                     └┘
pid                       └─┘       └────┘                     
st   ──────────────────────────────────────────────────────────────┘
220  end
st   └─┘
221  
222  theorem mem_uniformity_edist_inv_nat {s : set (α×α)} :
id                                             └─┘  
src                                            └─┘   
typ                                            └─┘  
223    s ∈ 𝓤 α ↔ (∃n:ℕ, ∀ a b : α, edist a b < n⁻¹ → (a, b) ∈ s) :=
id                        └───┘    └┘        
src                          └───┘       └┘         
typ                       └───┘    └┘        
doc        
224  begin
st   └─────
225    refine mem_uniformity_edist.trans ⟨λ hs, _, λ hs, _⟩,
id            └────────────────────────┘
src    └─────┘└────────────────────────┘  └──────┘ └─────┘
typ    └─────┘└────────────────────────┘  └──────┘ └─────┘
doc    └─────┘└────────────────────────┘  └──────┘ └─────┘
txt    └─────┘                            └──────┘ └─────┘
par    └─────┘                            └──────┘ └─────┘
pid                                      └──────┘ └─────┘
st   ─────────────────────────────────────────────────────┘└─
226    { rcases hs with ⟨ε, ε_pos, hε⟩,
id              └┘
src      └─────┘  └──────────────────┘
typ      └─────┘└┘└──────────────────┘
doc      └─────┘  └──────────────────┘
txt      └─────┘  └──────────────────┘
par      └─────┘  └──────────────────┘
pid              └──────────────────┘
st   ───┘└───────────────────────────┘└─
227      rcases ennreal.exists_inv_nat_lt (ne_of_gt ε_pos) with ⟨n, hn⟩,
id              └───────────────────────┘  └──────┘ └───┘
src      └─────┘└───────────────────────┘ └──────┘     └────────────┘
typ      └─────┘└───────────────────────┘ └──────┘└───┘└────────────┘
doc      └─────┘                                       └────────────┘
txt      └─────┘                                       └────────────┘
par      └─────┘                                       └────────────┘
pid                                                   └────────────┘
st   ─────────────────────────────────────────────────────────────────┘└─
228      exact ⟨n, λ a b hab, hε (lt_trans hab hn)⟩ },
id                           └┘  └──────┘     └┘
src      └────┘  └┘ └────────┘   └──────┘     └─┘
typ      └────┘ └┘ └────────┘└┘ └──────┘   └┘└─┘
doc      └────┘  └┘ └────────┘                └─┘
txt      └────┘  └┘ └────────┘                └─┘
par      └────┘  └┘ └────────┘                └─┘
pid             └┘ └────────┘                └┘
st   ──────────────────────────────────────────────┘└┘
229    { rcases hs with ⟨n, hn⟩,
id              └┘
src      └─────┘  └───────────┘
typ      └─────┘└┘└───────────┘
doc      └─────┘  └───────────┘
txt      └─────┘  └───────────┘
par      └─────┘  └───────────┘
pid              └───────────┘
st   ─────────────────────────┘└─
230      exact ⟨n⁻¹, ennreal.inv_pos.2 ennreal.coe_nat_ne_top, hn⟩ }
id              └┘  └─────────────┘   └────────────────────┘  └┘
src      └────┘  └┘└┘└─────────────┘└─┘└────────────────────┘└┘  └┘
typ      └────┘ └┘└┘└─────────────┘└─┘└────────────────────┘└┘└┘└┘
doc      └────┘    └┘               └─┘                      └┘  └┘
txt      └────┘    └┘               └─┘                      └┘  └┘
par      └────┘    └┘               └─┘                      └┘  └┘
pid               └┘               └─┘                      └┘  
st   ─────────────────────────────────────────────────────────────┘└─
231  end
st   ──┘
232  
233  theorem uniformity_edist_inv_nat :
234    𝓤 α = (⨅ n:ℕ, principal {p:α×α | edist p.1 p.2 < n⁻¹}) :=
id             └───────┘      └───┘      └┘
src             └───────┘        └───┘         └┘
typ            └───────┘      └───┘      └┘
doc               └───────┘
235  begin
st   └─────
236    refine eq_infi_of_mem_sets_iff_exists_mem (λ s, mem_uniformity_edist_inv_nat.trans _),
id            └────────────────────────────────┘       └────────────────────────────────┘
src    └─────┘└────────────────────────────────┘  └──┘└────────────────────────────────┘└─┘
typ    └─────┘└────────────────────────────────┘  └──┘└────────────────────────────────┘└─┘
doc    └─────┘                                    └──┘                                  └─┘
txt    └─────┘                                    └──┘                                  └─┘
par    └─────┘                                    └──┘                                  └─┘
pid                                              └──┘                                  └─┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
237    exact exists_congr (λn, by simp only [prod.forall, mem_principal_sets, subset_def, mem_set_of_eq])
id           └──────────┘                    └─────────┘  └────────────────┘  └────────┘  └───────────┘
src    └────┘└──────────┘  └─┘  └─────────┘└─────────┘└┘└────────────────┘└┘└────────┘└┘└───────────┘└┘
typ    └────┘└──────────┘  └─┘  └─────────┘└─────────┘└┘└────────────────┘└┘└────────┘└┘└───────────┘└┘
doc    └────┘              └─┘  └─────────┘           └┘                  └┘          └┘             └┘
txt    └────┘              └─┘  └─────────┘           └┘                  └┘          └┘             └┘
par    └────┘              └─┘  └─────────┘           └┘                  └┘          └┘             └┘
pid                       └─┘  └──────────┘           └┘                  └┘          └┘             └┘
st   ───────────────────────────┘└─────────────────────────────────────────────────────────────────────┘└┘
238  end
st   └─┘
239  
240  namespace emetric
241  
242  theorem uniformity_has_countable_basis : has_countable_basis (𝓤 α) :=
id                                            └─────────────────┘   
src                                           └─────────────────┘  
typ                                           └─────────────────┘   
doc                                           └─────────────────┘  
243  has_countable_basis_of_seq _ _ uniformity_edist_inv_nat
id   └────────────────────────┘     └──────────────────────┘
src  └────────────────────────┘     └──────────────────────┘
typ  └────────────────────────┘     └──────────────────────┘
244  
245  /-- ε-δ characterization of uniform continuity on emetric spaces -/
246  theorem uniform_continuous_iff [emetric_space β] {f : α → β} :
id                                   └───────────┘           
src                                  └───────────┘
typ                                  └───────────┘           
doc                                  └───────────┘
247    uniform_continuous f ↔ ∀ ε > 0, ∃ δ > 0,
id     └────────────────┘                
src    └────────────────┘                  
typ    └────────────────┘                
248      ∀{a b:α}, edist a b < δ → edist (f a) (f b) < ε :=
id                └───┘       └───┘          
src                └───┘          └───┘             
typ               └───┘       └───┘          
249  uniform_continuous_def.trans
id   └────────────────────┘└────┘
src  └────────────────────┘└────┘
typ  └────────────────────┘└────┘
250  ⟨λ H ε ε0, mem_uniformity_edist.1 $ H _ $ edist_mem_uniformity ε0,
id        └┘  └──────────────────┘         └──────────────────┘ └┘
src             └──────────────────┘          └──────────────────┘
typ       └┘  └──────────────────┘         └──────────────────┘ └┘
doc             └──────────────────┘           └──────────────────┘
251   λ H r ru,
id        └┘
typ       └┘
252    let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru, ⟨δ, δ0, hδ⟩ := H _ ε0 in
id     └─┘     └┘  └┘     └──────────────────┘  └┘     └┘  └┘     
src                       └──────────────────┘
typ    └─┘     └┘  └┘     └──────────────────┘  └┘     └┘  └┘     
doc                       └──────────────────┘
253    mem_uniformity_edist.2 ⟨δ, δ0, λ a b h, hε (hδ h)⟩⟩
id     └──────────────────┘                       
src    └──────────────────┘
typ    └──────────────────┘                       
doc    └──────────────────┘
254  
255  /-- ε-δ characterization of uniform embeddings on emetric spaces -/
256  theorem uniform_embedding_iff [emetric_space β] {f : α → β} :
id                                  └───────────┘           
src                                 └───────────┘
typ                                 └───────────┘           
doc                                 └───────────┘
257    uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧
id     └───────────────┘   └────────────────┘   └────────────────┘  
src    └───────────────┘    └────────────────┘    └────────────────┘   
typ    └───────────────┘   └────────────────┘   └────────────────┘  
258      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ :=
id                                 └───┘             └───┘    
src                                   └───┘                  └───┘     
typ                                └───┘             └───┘    
259  uniform_embedding_def'.trans $ and_congr iff.rfl $ and_congr iff.rfl
id   └────────────────────┘└────┘   └───────┘ └─────┘   └───────┘ └─────┘
src  └────────────────────┘└────┘   └───────┘ └─────┘   └───────┘ └─────┘
typ  └────────────────────┘└────┘   └───────┘ └─────┘   └───────┘ └─────┘
260  ⟨λ H δ δ0, let ⟨t, tu, ht⟩ := H _ (edist_mem_uniformity δ0),
id        └┘  └─┘     └┘  └┘         └──────────────────┘ └┘
src                                     └──────────────────┘
typ       └┘  └─┘     └┘  └┘         └──────────────────┘ └┘
doc                                     └──────────────────┘
261                 ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 tu in
id                     └┘  └┘     └──────────────────┘
src                                └──────────────────┘
typ                    └┘  └┘     └──────────────────┘
doc                                └──────────────────┘
262    ⟨ε, ε0, λ a b h, ht _ _ (hε h)⟩,
id                              
typ                             
263   λ H s su, let ⟨δ, δ0, hδ⟩ := mem_uniformity_edist.1 su, ⟨ε, ε0, hε⟩ := H _ δ0 in
id        └┘  └─┘     └┘  └┘     └──────────────────┘  └┘      └┘  └┘     
src                                └──────────────────┘
typ       └┘  └─┘     └┘  └┘     └──────────────────┘  └┘      └┘  └┘     
doc                                └──────────────────┘
264    ⟨_, edist_mem_uniformity ε0, λ a b h, hδ (hε h)⟩⟩
id         └──────────────────┘                  
src        └──────────────────┘
typ        └──────────────────┘                  
doc        └──────────────────┘
265  
266  /-- A map between emetric spaces is a uniform embedding if and only if the edistance between `f x`
267  and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/
268  theorem uniform_embedding_iff' [emetric_space β] {f : α → β} :
id                                   └───────────┘           
src                                  └───────────┘
typ                                  └───────────┘           
doc                                  └───────────┘
269    uniform_embedding f ↔
id     └───────────────┘  
src    └───────────────┘   
typ    └───────────────┘  
270    (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧
id                                └───┘       └───┘            
src                                  └───┘          └───┘                 
typ                               └───┘       └───┘            
271    (∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ) :=
id                                └───┘             └───┘    
src                                  └───┘                  └───┘     
typ                               └───┘             └───┘    
272  begin
st   └─────
273    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
274    { assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
275      exact ⟨uniform_continuous_iff.1 (uniform_embedding_iff.1 h).2.1,
id              └────────────────────┘
src      └────┘ └────────────────────┘└─┘                      └─┘ └──────
typ      └────┘ └────────────────────┘└─┘                      └─┘ └──────
doc      └────┘ └────────────────────┘└─┘                      └─┘ └──────
txt      └────┘                       └─┘                      └─┘ └──────
par      └────┘                       └─┘                      └─┘ └──────
pid                                  └─┘                      └─┘ └──────
st   ─────────────────────────────────────────────────────────────────────
276            (uniform_embedding_iff.1 h).2.2⟩ },
id              └───────────────────┘   
src  ─────────┘ └───────────────────┘└─┘ └─────┘
typ  ─────────┘ └───────────────────┘└─┘└─────┘
doc  ─────────┘ └───────────────────┘└─┘ └─────┘
txt  ─────────┘                      └─┘ └─────┘
par  ─────────┘                      └─┘ └─────┘
pid  ─────────┘                      └─┘ └────┘
st   ──────────────────────────────────────────┘└┘
277    { rintros ⟨h₁, h₂⟩,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid             └───────┘
st   ───────────────────┘└─
278      refine uniform_embedding_iff.2 ⟨_, uniform_continuous_iff.2 h₁, h₂⟩,
id              └───────────────────┘       └────────────────────┘   └┘  └┘
src      └─────┘└───────────────────┘└─┘ └─┘└────────────────────┘└─┘  └┘  
typ      └─────┘└───────────────────┘└─┘ └─┘└────────────────────┘└─┘└┘└┘└┘
doc      └─────┘└───────────────────┘└─┘ └─┘└────────────────────┘└─┘  └┘  
txt      └─────┘                     └─┘ └─┘                      └─┘  └┘  
par      └─────┘                     └─┘ └─┘                      └─┘  └┘  
pid                                 └─┘ └─┘                      └─┘  └┘  
st   ──────────────────────────────────────────────────────────────────────┘└─
279      assume x y hxy,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ─────────────────┘└─
280      have : edist x y ≤ 0,
id              └───┘   
src      └─────┘└───┘  └┘
typ      └─────┘└───┘└┘
doc      └─────┘        └┘
txt      └─────┘        └┘
par      └─────┘        └┘
pid      └───┘└┘        
st   ───────────────────────┘└─
281      { refine le_of_forall_lt' (λδ δpos, _),
id                └──────────────┘
src        └─────┘└──────────────┘  └────────┘
typ        └─────┘└──────────────┘  └────────┘
doc        └─────┘                  └────────┘
txt        └─────┘                  └────────┘
par        └─────┘                  └────────┘
pid                                └────────┘
st   ─────┘└──────────────────────────────────┘└─
282        rcases h₂ δ δpos with ⟨ε, εpos, hε⟩,
id                └┘  └──┘
src        └─────┘       └─────────────────┘
typ        └─────┘└┘└──┘└─────────────────┘
doc        └─────┘       └─────────────────┘
txt        └─────┘       └─────────────────┘
par        └─────┘       └─────────────────┘
pid                     └─────────────────┘
st   ────────────────────────────────────────┘└─
283        have : edist (f x) (f y) < ε, by simpa [hxy],
id                └───┘                       └─┘
src        └─────┘└───┘   └┘   └┘      └─────┘   
typ        └─────┘└───┘  └┘ └┘     └─────┘└─┘
doc        └─────┘        └┘   └┘       └─────┘   
txt        └─────┘        └┘   └┘       └─────┘   
par        └─────┘        └┘   └┘       └─────┘   
pid        └───┘└┘        └┘   └┘               
st   ─────────────────────────────────┘                └─
284        exact hε this },
id               └┘ └──┘
src        └────┘      
typ        └────┘└┘└──┘
doc        └────┘      
txt        └────┘      
par        └────┘      
pid                   
st   ───────────────────┘└┘
285      simpa using this }
id                   └──┘
src      └──────────┘    
typ      └──────────┘└──┘
doc      └──────────┘    
txt      └──────────┘    
par      └──────────┘    
pid           └────┘    
st   ────────────────────┘└─
286  end
st   ──┘
287  
288  /-- ε-δ characterization of Cauchy sequences on emetric spaces -/
289  protected lemma cauchy_iff {f : filter α} :
id                                   └────┘ 
src                                  └────┘
typ                                  └────┘ 
290    cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x y ∈ t, edist x y < ε :=
id     └────┘                            └───┘    
src    └────┘                                   └───┘     
typ    └────┘                            └───┘    
doc    └────┘
291  cauchy_iff.trans $ and_congr iff.rfl
id   └────────┘└────┘   └───────┘ └─────┘
src  └────────┘└────┘   └───────┘ └─────┘
typ  └────────┘└────┘   └───────┘ └─────┘
292  ⟨λ H ε ε0, let ⟨t, tf, ts⟩ := H _ (edist_mem_uniformity ε0) in
id        └┘  └─┘    └┘  └┘         └──────────────────┘ └┘
src                                     └──────────────────┘
typ       └┘  └─┘    └┘  └┘         └──────────────────┘ └┘
doc                                     └──────────────────┘
293     ⟨t, tf, λ x y xt yt, @ts (x, y) ⟨xt, yt⟩⟩,
id                  └┘ └┘           └┘  └┘
src                              
typ                 └┘ └┘           └┘  └┘
294   λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru,
id        └┘  └─┘    └┘  └┘     └──────────────────┘  └┘
src                                └──────────────────┘
typ       └┘  └─┘    └┘  └┘     └──────────────────┘  └┘
doc                                └──────────────────┘
295                 ⟨t, tf, h⟩ := H ε ε0 in
id                     └┘       
typ                    └┘       
296     ⟨t, tf, λ ⟨x, y⟩ ⟨hx, hy⟩, hε (h x y hx hy)⟩⟩
id                    └┘  └┘
typ                   └┘  └┘
297  
298  /-- A very useful criterion to show that a space is complete is to show that all sequences
299  which satisfy a bound of the form `edist (u n) (u m) < B N` for all `n m ≥ N` are
300  converging. This is often applied for `B N = 2^{-N}`, i.e., with a very fast convergence to
301  `0`, which makes it possible to use arguments of converging series, while this is impossible
302  to do in general for arbitrary Cauchy sequences. -/
303  theorem complete_of_convergent_controlled_sequences (B : ℕ → ennreal) (hB : ∀n, 0 < B n)
id                                                               └─────┘               
src                                                              └─────┘              
typ                                                              └─────┘               
doc                                                               └─────┘
304    (H : ∀u : ℕ → α, (∀N n m : ℕ, N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃x, tendsto u at_top (𝓝 x)) :
id                                        └───┘                └─────┘  └────┘   
src                                              └───┘                       └─────┘   └────┘  
typ                                       └───┘                └─────┘  └────┘   
doc                                                                                 └─────┘   └────┘  
305    complete_space α :=
id     └────────────┘ 
src    └────────────┘
typ    └────────────┘ 
doc    └────────────┘
306  uniform_space.complete_of_convergent_controlled_sequences
id   └───────────────────────────────────────────────────────┘
src  └───────────────────────────────────────────────────────┘
typ  └───────────────────────────────────────────────────────┘
doc  └───────────────────────────────────────────────────────┘
307    uniformity_has_countable_basis
id     └────────────────────────────┘
src    └────────────────────────────┘
typ    └────────────────────────────┘
308    (λ n, {p:α×α | edist p.1 p.2 < B n}) (λ n, edist_mem_uniformity $ hB n) H
id               └───┘               └──────────────────┘   └┘   
src                 └───┘                    └──────────────────┘
typ              └───┘               └──────────────────┘   └┘   
doc                                               └──────────────────┘
309  
310  /-- A sequentially complete emetric space is complete. -/
311  theorem complete_of_cauchy_seq_tendsto :
312    (∀ u : ℕ → α, cauchy_seq u → ∃a, tendsto u at_top (𝓝 a)) → complete_space α :=
id               └────────┘     └─────┘  └────┘        └────────────┘ 
src                 └────────┘       └─────┘   └────┘         └────────────┘
typ              └────────┘     └─────┘  └────┘        └────────────┘ 
doc                  └────────┘         └─────┘   └────┘         └────────────┘
313  uniform_space.complete_of_cauchy_seq_tendsto uniformity_has_countable_basis
id   └──────────────────────────────────────────┘ └────────────────────────────┘
src  └──────────────────────────────────────────┘ └────────────────────────────┘
typ  └──────────────────────────────────────────┘ └────────────────────────────┘
doc  └──────────────────────────────────────────┘
314  
315  end emetric
316  
317  open emetric
318  
319  /-- An emetric space is separated -/
320  @[priority 100] -- see Note [lower instance priority]
321  instance to_separated : separated α :=
id                           └───────┘ 
src                          └───────┘
typ                          └───────┘ 
322  separated_def.2 $ λ x y h, eq_of_forall_edist_le $
id   └───────────┘          └───────────────────┘
src  └───────────┘             └───────────────────┘
typ  └───────────┘          └───────────────────┘
doc                             └───────────────────┘
323  λ ε ε0, le_of_lt (h _ (edist_mem_uniformity ε0))
id      └┘  └──────┘      └──────────────────┘ └┘
src          └──────┘       └──────────────────┘
typ     └┘  └──────┘      └──────────────────┘ └┘
doc                         └──────────────────┘
324  
325  /-- Auxiliary function to replace the uniformity on an emetric space with
326  a uniformity which is equal to the original one, but maybe not defeq.
327  This is useful if one wants to construct an emetric space with a
328  specified uniformity. -/
329  def emetric_space.replace_uniformity {α} [U : uniform_space α] (m : emetric_space α)
id                                                 └───────────┘        └───────────┘ 
src                                                └───────────┘         └───────────┘
typ                                                └───────────┘        └───────────┘ 
doc                                                └───────────┘         └───────────┘
330    (H : @uniformity _ U = @uniformity _ (emetric_space.to_uniform_space α)) :
id           └────────┘      └────────┘    └────────────────────────────┘ 
src          └────────┘       └────────┘    └────────────────────────────┘
typ          └────────┘      └────────┘    └────────────────────────────┘ 
doc          └────────┘        └────────┘
331    emetric_space α :=
id     └───────────┘ 
src    └───────────┘
typ    └───────────┘ 
doc    └───────────┘
332  { edist               := @edist _ m.to_has_edist,
id                             └───┘   └───────────┘
src                            └───┘    └───────────┘
typ                            └───┘   └───────────┘
333    edist_self          := edist_self,
id                            └────────┘
src                           └────────┘
typ                           └────────┘
334    eq_of_edist_eq_zero := @eq_of_edist_eq_zero _ _,
id                             └─────────────────┘
src                            └─────────────────┘
typ                            └─────────────────┘
335    edist_comm          := edist_comm,
id                            └────────┘
src                           └────────┘
typ                           └────────┘
336    edist_triangle      := edist_triangle,
id                            └────────────┘
src                           └────────────┘
typ                           └────────────┘
337    to_uniform_space    := U,
id                            
typ                           
338    uniformity_edist    := H.trans (@emetric_space.uniformity_edist α _) }
id                            └────┘   └────────────────────────────┘ 
src                            └────┘   └────────────────────────────┘
typ                           └────┘   └────────────────────────────┘ 
339  
340  /-- The extended metric induced by an injective function taking values in an emetric space. -/
341  def emetric_space.induced {α β} (f : α → β) (hf : function.injective f)
id                                                   └────────────────┘ 
src                                                    └────────────────┘
typ                                                  └────────────────┘ 
342    (m : emetric_space β) : emetric_space α :=
id          └───────────┘     └───────────┘ 
src         └───────────┘      └───────────┘
typ         └───────────┘     └───────────┘ 
doc         └───────────┘      └───────────┘
343  { edist               := λ x y, edist (f x) (f y),
id                                 └───┘       
src                                  └───┘
typ                                └───┘       
344    edist_self          := λ x, edist_self _,
id                                └────────┘
src                                └────────┘
typ                               └────────┘
345    eq_of_edist_eq_zero := λ x y h, hf (edist_eq_zero.1 h),
id                                  └┘  └───────────┘  
src                                        └───────────┘
typ                                 └┘  └───────────┘  
doc                                        └───────────┘
346    edist_comm          := λ x y, edist_comm _ _,
id                                 └────────┘
src                                  └────────┘
typ                                └────────┘
347    edist_triangle      := λ x y z, edist_triangle _ _ _,
id                                  └────────────┘
src                                    └────────────┘
typ                                 └────────────┘
348    to_uniform_space    := uniform_space.comap f m.to_uniform_space,
id                            └─────────────────┘  └───────────────┘
src                           └─────────────────┘    └───────────────┘
typ                           └─────────────────┘  └───────────────┘
doc                           └─────────────────┘
349    uniformity_edist    := begin
st                            └─────
350      apply @uniformity_dist_of_mem_uniformity _ _ _ _ _ (λ x y, edist (f x) (f y)),
id              └───────────────────────────────┘                   └───┘        
src      └────┘ └───────────────────────────────┘└─────────┘  └────┘└───┘   └┘   └┘
typ      └────┘ └───────────────────────────────┘└─────────┘  └────┘└───┘   └┘  └┘
doc      └────┘ └───────────────────────────────┘└─────────┘  └────┘        └┘   └┘
txt      └────┘                                  └─────────┘  └────┘        └┘   └┘
par      └────┘                                  └─────────┘  └────┘        └┘   └┘
pid                                             └─────────┘  └────┘        └┘   └┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
351      refine λ s, mem_comap_sets.trans _,
id                   └──────────────────┘
src      └─────┘ └──┘└──────────────────┘└┘
typ      └─────┘ └──┘└──────────────────┘└┘
doc      └─────┘ └──┘                    └┘
txt      └─────┘ └──┘                    └┘
par      └─────┘ └──┘                    └┘
pid             └──┘                    └┘
st   ─────────────────────────────────────┘└─
352      split; intro H,
src      └───┘  └─────┘
typ      └───┘  └─────┘
doc      └───┘  └─────┘
txt      └───┘  └─────┘
par      └───┘  └─────┘
pid                  └┘
st   ─────────────────┘└─
353      { rcases H with ⟨r, ru, rs⟩,
id                
src        └─────┘ └───────────────┘
typ        └─────┘└───────────────┘
doc        └─────┘ └───────────────┘
txt        └─────┘ └───────────────┘
par        └─────┘ └───────────────┘
pid               └───────────────┘
st   ─────┘└───────────────────────┘└─
354        rcases mem_uniformity_edist.1 ru with ⟨ε, ε0, hε⟩,
id                └──────────────────┘   └┘
src        └─────┘└──────────────────┘└─┘  └───────────────┘
typ        └─────┘└──────────────────┘└─┘└┘└───────────────┘
doc        └─────┘└──────────────────┘└─┘  └───────────────┘
txt        └─────┘                    └─┘  └───────────────┘
par        └─────┘                    └─┘  └───────────────┘
pid                                  └─┘  └───────────────┘
st   ──────────────────────────────────────────────────────┘└─
355        refine ⟨ε, ε0, λ a b h, rs (hε _)⟩, exact h },
id                   └┘           └┘  └┘            
src        └─────┘  └┘  └┘ └──────┘     └──┘  └────┘ 
typ        └─────┘ └┘└┘└┘ └──────┘└┘ └┘└──┘  └────┘
doc        └─────┘  └┘  └┘ └──────┘     └──┘  └────┘ 
txt        └─────┘  └┘  └┘ └──────┘     └──┘  └────┘ 
par        └─────┘  └┘  └┘ └──────┘     └──┘  └────┘ 
pid                └┘  └┘ └──────┘     └──┘        
st   ───────────────────────────────────────┘└────────┘└┘
356      { rcases H with ⟨ε, ε0, hε⟩,
id                
src        └─────┘ └───────────────┘
typ        └─────┘└───────────────┘
doc        └─────┘ └───────────────┘
txt        └─────┘ └───────────────┘
par        └─────┘ └───────────────┘
pid               └───────────────┘
st   ──────────────────────────────┘└─
357        exact ⟨_, edist_mem_uniformity ε0, λ ⟨a, b⟩, hε⟩ }
id                   └──────────────────┘ └┘            └┘
src        └────┘ └─┘└──────────────────┘  └┘ └┘ └┘ └─┘  └┘
typ        └────┘ └─┘└──────────────────┘└┘└┘ └┘ └┘ └─┘└┘└┘
doc        └────┘ └─┘└──────────────────┘  └┘ └┘ └┘ └─┘  └┘
txt        └────┘ └─┘                      └┘ └┘ └┘ └─┘  └┘
par        └────┘ └─┘                      └┘ └┘ └┘ └─┘  └┘
pid              └─┘                      └┘ └┘ └┘ └─┘  
st   ──────────────────────────────────────────────────────┘└─
358    end }
st   ────┘
359  
360  /-- Emetric space instance on subsets of emetric spaces -/
361  instance {α : Type*} {p : α → Prop} [t : emetric_space α] : emetric_space (subtype p) :=
id                                           └───────────┘     └───────────┘  └─────┘ 
src                                           └───────────┘      └───────────┘  └─────┘
typ                                          └───────────┘     └───────────┘  └─────┘ 
doc                                           └───────────┘      └───────────┘
362  t.induced subtype.val (λ x y, subtype.eq)
id   └──────┘ └─────────┘       └────────┘
src   └──────┘ └─────────┘         └────────┘
typ  └──────┘ └─────────┘       └────────┘
doc   └──────┘
363  
364  /-- The extended distance on a subset of an emetric space is the restriction of
365  the original distance, by definition -/
366  theorem subtype.edist_eq {p : α → Prop} (x y : subtype p) : edist x y = edist x.1 y.1 := rfl
id                                                 └─────┘     └───┘    └───┘        └─┘
src                                                 └─────┘      └───┘      └───┘          └─┘
typ                                                └─────┘     └───┘    └───┘        └─┘
367  
368  /-- The product of two emetric spaces, with the max distance, is an extended
369  metric spaces. We make sure that the uniform structure thus constructed is the one
370  corresponding to the product of uniform spaces, to avoid diamond problems. -/
371  instance prod.emetric_space_max [emetric_space β] : emetric_space (α × β) :=
id                                    └───────────┘     └───────────┘    
src                                   └───────────┘      └───────────┘    
typ                                   └───────────┘     └───────────┘    
doc                                   └───────────┘      └───────────┘
372  { edist := λ x y, max (edist x.1 y.1) (edist x.2 y.2),
id                   └─┘  └───┘       └───┘   
src                    └─┘  └───┘         └───┘     
typ                  └─┘  └───┘       └───┘   
373    edist_self := λ x, by simp,
id                     
src                          └──┘
typ                         └──┘
doc                          └──┘
txt                          └──┘
par                          └──┘
st                          └───┘
374    eq_of_edist_eq_zero := λ x y h, begin
id                                
typ                               
st                                     └─────
375      cases max_le_iff.1 (le_of_eq h) with h₁ h₂,
id             └────────┘    └──────┘ 
src      └────┘└────────┘└─┘ └──────┘ └──────────┘
typ      └────┘└────────┘└─┘ └──────┘└──────────┘
doc      └────┘          └─┘          └──────────┘
txt      └────┘          └─┘          └──────────┘
par      └────┘          └─┘          └──────────┘
pid                     └─┘          └─────────┘
st   ─────────────────────────────────────────────┘└─
376      have A : x.fst = y.fst := edist_le_zero.1 h₁,
id                └───┘  └───┘    └───────────┘   └┘
src      └───────┘└───┘└───┘└──┘└───────────┘└─┘
typ      └───────┘└───┘└───┘└──┘└───────────┘└─┘└┘
doc      └───────┘           └──┘             └─┘
txt      └───────┘           └──┘             └─┘
par      └───────┘           └──┘             └─┘
pid      └────┘└─┘           └──┘             └─┘
st   ───────────────────────────────────────────────┘└─
377      have B : x.snd = y.snd := edist_le_zero.1 h₂,
id                └───┘   └───┘    └───────────┘   └┘
src      └───────┘└───┘ └───┘└──┘└───────────┘└─┘
typ      └───────┘└───┘ └───┘└──┘└───────────┘└─┘└┘
doc      └───────┘           └──┘             └─┘
txt      └───────┘           └──┘             └─┘
par      └───────┘           └──┘             └─┘
pid      └────┘└─┘           └──┘             └─┘
st   ───────────────────────────────────────────────┘└─
378      exact prod.ext_iff.2 ⟨A, B⟩
id             └──────────┘      
src      └────┘└──────────┘└─┘  └┘ └─
typ      └────┘└──────────┘└─┘ └┘└─
doc      └────┘            └─┘  └┘ └─
txt      └────┘            └─┘  └┘ └─
par      └────┘            └─┘  └┘ └─
pid                       └─┘  └┘ 
st   ────────────────────────────────
379    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
380    edist_comm := λ x y, by simp [edist_comm],
id                                 └────────┘
src                            └────┘└────────┘
typ                          └────┘└────────┘
doc                            └────┘          
txt                            └────┘          
par                            └────┘          
pid                                          
st                            └────────────────┘
381    edist_triangle := λ x y z, max_le
id                             └────┘
src                               └────┘
typ                            └────┘
382      (le_trans (edist_triangle _ _ _) (add_le_add' (le_max_left _ _) (le_max_left _ _)))
id        └──────┘  └────────────┘         └─────────┘  └─────────┘       └─────────┘
src       └──────┘  └────────────┘         └─────────┘  └─────────┘       └─────────┘
typ       └──────┘  └────────────┘         └─────────┘  └─────────┘       └─────────┘
383      (le_trans (edist_triangle _ _ _) (add_le_add' (le_max_right _ _) (le_max_right _ _))),
id        └──────┘  └────────────┘         └─────────┘  └──────────┘       └──────────┘
src       └──────┘  └────────────┘         └─────────┘  └──────────┘       └──────────┘
typ       └──────┘  └────────────┘         └─────────┘  └──────────┘       └──────────┘
384    uniformity_edist := begin
st                         └─────
385      refine uniformity_prod.trans _,
id              └───────────────────┘
src      └─────┘└───────────────────┘└┘
typ      └─────┘└───────────────────┘└┘
doc      └─────┘                     └┘
txt      └─────┘                     └┘
par      └─────┘                     └┘
pid                                 └┘
st   ─────────────────────────────────┘└─
386      simp [emetric_space.uniformity_edist, comap_infi],
id             └────────────────────────────┘  └────────┘
src      └────┘└────────────────────────────┘└┘└────────┘
typ      └────┘└────────────────────────────┘└┘└────────┘
doc      └────┘                              └┘          
txt      └────┘                              └┘          
par      └────┘                              └┘          
pid                                        └┘          
st   ────────────────────────────────────────────────────┘└─
387      rw ← infi_inf_eq, congr, funext,
id            └─────────┘
src      └───┘└─────────┘  └───┘  └────┘
typ      └───┘└─────────┘  └───┘  └────┘
doc      └───┘                    └────┘
txt      └───┘             └───┘  └────┘
par      └───┘             └───┘  └────┘
pid        └─┘
st   ───────────────────┘└─────┘└──────┘└─
388      rw ← infi_inf_eq, congr, funext,
id            └─────────┘
src      └───┘└─────────┘  └───┘  └────┘
typ      └───┘└─────────┘  └───┘  └────┘
doc      └───┘                    └────┘
txt      └───┘             └───┘  └────┘
par      └───┘             └───┘  └────┘
pid        └─┘
st   ───────────────────┘└─────┘└──────┘└─
389      simp [inf_principal, ext_iff, max_lt_iff]
id             └───────────┘  └─────┘  └────────┘
src      └────┘└───────────┘└┘└─────┘└┘└────────┘└─
typ      └────┘└───────────┘└┘└─────┘└┘└────────┘└─
doc      └────┘             └┘       └┘          └─
txt      └────┘             └┘       └┘          └─
par      └────┘             └┘       └┘          └─
pid                       └┘       └┘          
st   ──────────────────────────────────────────────
390    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
391    to_uniform_space := prod.uniform_space }
id                         └────────────────┘
src                        └────────────────┘
typ                        └────────────────┘
392  
393  section pi
394  open finset
395  variables {π : β → Type*} [fintype β]
id                              └─────┘
src                             └─────┘
typ                             └─────┘
doc                             └─────┘
396  
397  /-- The product of a finite number of emetric spaces, with the max distance, is still
398  an emetric space.
399  This construction would also work for infinite products, but it would not give rise
400  to the product topology. Hence, we only formalize it in the good situation of finitely many
401  spaces. -/
402  instance emetric_space_pi [∀b, emetric_space (π b)] : emetric_space (Πb, π b) :=
id                                 └───────────┘        └───────────┘      
src                                 └───────────┘          └───────────┘
typ                                └───────────┘        └───────────┘      
doc                                 └───────────┘          └───────────┘
403  { edist := λ f g, finset.sup univ (λb, edist (f b) (g b)),
id                   └────────┘ └──┘     └───┘       
src                    └────────┘ └──┘      └───┘
typ                  └────────┘ └──┘     └───┘       
doc                    └────────┘ └──┘
404    edist_self := assume f, bot_unique $ finset.sup_le $ by simp,
id                            └────────┘   └───────────┘
src                            └────────┘   └───────────┘      └──┘
typ                           └────────┘   └───────────┘      └──┘
doc                                                            └──┘
txt                                                            └──┘
par                                                            └──┘
st                                                            └───┘
405    edist_comm := assume f g, by unfold edist; congr; funext a; exact edist_comm _ _,
id                                                                     └────────┘
src                                 └──────────┘  └───┘  └──────┘  └────┘└────────┘└──┘
typ                               └──────────┘  └───┘  └──────┘  └────┘└────────┘└──┘
doc                                 └──────────┘         └──────┘  └────┘          └──┘
txt                                 └──────────┘  └───┘  └──────┘  └────┘          └──┘
par                                 └──────────┘  └───┘  └──────┘  └────┘          └──┘
pid                                       └────┘               └┘                 └──┘
st                                 └──────────────────────────────────────────────────┘
406    edist_triangle := assume f g h,
id                                
typ                               
407      begin
st       └─────
408        simp only [finset.sup_le_iff],
id                    └───────────────┘
src        └─────────┘└───────────────┘
typ        └─────────┘└───────────────┘
doc        └─────────┘                 
txt        └─────────┘                 
par        └─────────┘                 
pid            └──┘└┘                 
st   ──────────────────────────────────┘└─
409        assume b hb,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ────────────────┘└─
410        exact le_trans (edist_triangle _ (g b) _) (add_le_add' (le_sup hb) (le_sup hb))
id               └──────┘  └────────────┘           └─────────┘              └────┘ └┘
src        └────┘└──────┘ └────────────┘└─┘   └───┘ └─────────┘         └┘ └────┘  └──
typ        └────┘└──────┘ └────────────┘└─┘ └───┘ └─────────┘         └┘ └────┘└┘└──
doc        └────┘                       └─┘   └───┘                     └┘         └──
txt        └────┘                       └─┘   └───┘                     └┘         └──
par        └────┘                       └─┘   └───┘                     └┘         └──
pid                                    └─┘   └───┘                     └┘         └┘
st   ──────────────────────────────────────────────────────────────────────────────────────
411      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
412    eq_of_edist_eq_zero := assume f g eq0,
id                                     └─┘
typ                                    └─┘
413      begin
st       └─────
414        have eq1 : sup univ (λ (b : β), edist (f b) (g b)) ≤ 0 := le_of_eq eq0,
id                    └─┘ └──┘            └───┘                  └──────┘ └─┘
src        └─────────┘└─┘└──┘  └────┘ └─┘└───┘   └┘   └─┘└────┘└──────┘
typ        └─────────┘└─┘└──┘  └────┘└─┘└───┘  └┘  └─┘└────┘└──────┘└─┘
doc        └─────────┘└─┘└──┘  └────┘ └─┘        └┘   └─┘ └────┘        
txt        └─────────┘         └────┘ └─┘        └┘   └─┘ └────┘        
par        └─────────┘         └────┘ └─┘        └┘   └─┘ └────┘        
pid        └──────┘└─┘         └────┘ └─┘        └┘   └─┘ └───┘        
st   ───────────────────────────────────────────────────────────────────────────┘└─
415        simp only [finset.sup_le_iff] at eq1,
id                    └───────────────┘
src        └─────────┘└───────────────┘└──────┘
typ        └─────────┘└───────────────┘└──────┘
doc        └─────────┘                 └──────┘
txt        └─────────┘                 └──────┘
par        └─────────┘                 └──────┘
pid            └──┘└┘                 └────┘
st   ─────────────────────────────────────────┘└─
416        exact (funext $ assume b, edist_le_zero.1 $ eq1 b $ mem_univ b),
id                └────┘             └───────────┘     └─┘     └──────┘
src        └────┘ └────┘       └──┘└───────────┘└─┘      └──────┘ 
typ        └────┘ └────┘       └──┘└───────────┘└─┘ └─┘  └──────┘ 
doc        └────┘              └──┘             └─┘               
txt        └────┘              └──┘             └─┘               
par        └────┘              └──┘             └─┘               
pid                           └──┘             └─┘               
st   ────────────────────────────────────────────────────────────────────┘└─
417      end,
st   ──────┘
418    to_uniform_space := Pi.uniform_space _,
id                         └──────────────┘
src                        └──────────────┘
typ                        └──────────────┘
419    uniformity_edist := begin
st                         └─────
420      simp only [Pi.uniformity, emetric_space.uniformity_edist, comap_infi, gt_iff_lt, preimage_set_of_eq,
id                  └───────────┘  └────────────────────────────┘  └────────┘  └───────┘  └────────────────┘
src      └─────────┘└───────────┘└┘└────────────────────────────┘└┘└────────┘└┘└───────┘└┘└────────────────┘└─
typ      └─────────┘└───────────┘└┘└────────────────────────────┘└┘└────────┘└┘└───────┘└┘└────────────────┘└─
doc      └─────────┘             └┘                              └┘          └┘         └┘                  └─
txt      └─────────┘             └┘                              └┘          └┘         └┘                  └─
par      └─────────┘             └┘                              └┘          └┘         └┘                  └─
pid          └──┘└┘             └┘                              └┘          └┘         └┘                  └─
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────
421            comap_principal],
id             └─────────────┘
src  ─────────┘└─────────────┘
typ  ─────────┘└─────────────┘
doc  ─────────┘               
txt  ─────────┘               
par  ─────────┘               
pid  ─────────┘               
st   ─────────────────────────┘└─
422      rw infi_comm, congr, funext ε,
id          └───────┘
src      └─┘└───────┘  └───┘  └──────┘
typ      └─┘└───────┘  └───┘  └──────┘
doc      └─┘                  └──────┘
txt      └─┘           └───┘  └──────┘
par      └─┘           └───┘  └──────┘
pid                                └┘
st   ───────────────┘└─────┘└────────┘└─
423      rw infi_comm, congr, funext εpos,
id          └───────┘
src      └─┘└───────┘  └───┘  └─────────┘
typ      └─┘└───────┘  └───┘  └─────────┘
doc      └─┘                  └─────────┘
txt      └─┘           └───┘  └─────────┘
par      └─┘           └───┘  └─────────┘
pid                                └───┘
st   ───────────────┘└─────┘└───────────┘└─
424      change 0 < ε at εpos,
id                 
src      └───────┘ └──────┘
typ      └───────┘└──────┘
doc      └───────┘  └──────┘
txt      └───────┘  └──────┘
par      └───────┘  └──────┘
pid            └─┘  └─────┘
st   ───────────────────────┘└─
425      simp [ext_iff, εpos]
id             └─────┘  └──┘
src      └────┘└─────┘└┘    └─
typ      └────┘└─────┘└┘└──┘└─
doc      └────┘       └┘    └─
txt      └────┘       └┘    └─
par      └────┘       └┘    └─
pid                 └┘    
st   ─────────────────────────
426    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
427  
428  end pi
429  
430  namespace emetric
431  variables {x y z : α} {ε ε₁ ε₂ : ennreal} {s : set α}
id                                    └─────┘       └─┘
src                                   └─────┘       └─┘
typ                                   └─────┘       └─┘
doc                                   └─────┘
432  
433  /-- `emetric.ball x ε` is the set of all points `y` with `edist y x < ε` -/
434  def ball (x : α) (ε : ennreal) : set α := {y | edist y x < ε}
id                        └─────┘    └─┘        └───┘    
src                        └─────┘    └─┘          └───┘     
typ                       └─────┘    └─┘        └───┘    
doc                        └─────┘
435  
436  @[simp] theorem mem_ball : y ∈ ball x ε ↔ edist y x < ε := iff.rfl
id                                └──┘    └───┘        └─────┘
src                                └──┘      └───┘           └─────┘
typ                               └──┘    └───┘        └─────┘
doc    └──┘                         └──┘
437  
438  theorem mem_ball' : y ∈ ball x ε ↔ edist x y < ε := by rw edist_comm; refl
id                         └──┘    └───┘              └────────┘
src                         └──┘      └───┘              └─┘└────────┘  └────
typ                        └──┘    └───┘           └─┘└────────┘  └────
doc                          └──┘                           └─┘            └────
txt                                                         └─┘            └────
par                                                         └─┘            └────
pid                                                                           
st                                                         └────────────────────
439  
src  
typ  
doc  
txt  
par  
pid  
st   
440  /-- `emetric.closed_ball x ε` is the set of all points `y` with `edist y x ≤ ε` -/
441  def closed_ball (x : α) (ε : ennreal) := {y | edist y x ≤ ε}
id                               └─────┘        └───┘    
src                               └─────┘         └───┘     
typ                              └─────┘        └───┘    
doc                               └─────┘
442  
443  @[simp] theorem mem_closed_ball : y ∈ closed_ball x ε ↔ edist y x ≤ ε := iff.rfl
id                                       └─────────┘    └───┘        └─────┘
src                                       └─────────┘      └───┘           └─────┘
typ                                      └─────────┘    └───┘        └─────┘
doc    └──┘                                └─────────┘
444  
445  theorem ball_subset_closed_ball : ball x ε ⊆ closed_ball x ε :=
id                                     └──┘    └─────────┘  
src                                    └──┘      └─────────┘
typ                                    └──┘    └─────────┘  
doc                                    └──┘       └─────────┘
446  assume y, by simp; intros h; apply le_of_lt h
id                                     └──────┘ 
src               └──┘  └──────┘  └────┘└──────┘ 
typ              └──┘  └──────┘  └────┘└──────┘
doc               └──┘  └──────┘  └────┘         
txt               └──┘  └──────┘  └────┘         
par               └──┘  └──────┘  └────┘         
pid                           └┘                
st               └─────────────────────────────────
447  
src  
typ  
doc  
txt  
par  
pid  
st   
448  theorem pos_of_mem_ball (hy : y ∈ ball x ε) : 0 < ε :=
id                                   └──┘         
src                                   └──┘          
typ                                  └──┘         
doc                                    └──┘
449  lt_of_le_of_lt (zero_le _) hy
id   └────────────┘  └─────┘    └┘
src  └────────────┘  └─────┘
typ  └────────────┘  └─────┘    └┘
450  
451  theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε :=
id                                       └──┘  
src                                        └──┘
typ                                      └──┘  
doc                                          └──┘
452  show edist x x < ε, by rw edist_self; assumption
id        └───┘            └────────┘
src       └───┘            └─┘└────────┘  └──────────
typ       └───┘         └─┘└────────┘  └──────────
doc                         └─┘            └──────────
txt                         └─┘            └──────────
par                         └─┘            └──────────
pid                                                 
st                         └──────────────────────────
453  
src  
typ  
doc  
txt  
par  
pid  
st   
454  theorem mem_closed_ball_self : x ∈ closed_ball x ε :=
id                                    └─────────┘  
src                                    └─────────┘
typ                                   └─────────┘  
doc                                     └─────────┘
455  show edist x x ≤ ε, by rw edist_self; exact bot_le
id        └───┘            └────────┘        └────┘
src       └───┘            └─┘└────────┘  └────┘└────┘
typ       └───┘         └─┘└────────┘  └────┘└────┘
doc                         └─┘            └────┘      
txt                         └─┘            └────┘      
par                         └─┘            └────┘      
pid                                                  
st                         └────────────────────────────
456  
src  
typ  
doc  
txt  
par  
pid  
st   
457  theorem mem_ball_comm : x ∈ ball y ε ↔ y ∈ ball x ε :=
id                             └──┘      └──┘  
src                             └──┘         └──┘
typ                            └──┘      └──┘  
doc                              └──┘           └──┘
458  by simp [edist_comm]
id            └────────┘
src     └────┘└────────┘└─
typ     └────┘└────────┘└─
doc     └────┘          └─
txt     └────┘          └─
par     └────┘          └─
pid                   
st     └──────────────────
459  
src  
typ  
doc  
txt  
par  
pid  
st   
460  theorem ball_subset_ball (h : ε₁ ≤ ε₂) : ball x ε₁ ⊆ ball x ε₂ :=
id                                 └┘  └┘    └──┘  └┘  └──┘  └┘
src                                          └──┘       └──┘
typ                                └┘  └┘    └──┘  └┘  └──┘  └┘
doc                                           └──┘        └──┘
461  λ y (yx : _ < ε₁), lt_of_lt_of_le yx h
id               └┘   └────────────┘ └┘ 
src                    └────────────┘
typ              └┘   └────────────┘ └┘ 
462  
463  theorem closed_ball_subset_closed_ball (h : ε₁ ≤ ε₂) :
id                                               └┘  └┘
src                                                 
typ                                              └┘  └┘
464    closed_ball x ε₁ ⊆ closed_ball x ε₂ :=
id     └─────────┘  └┘  └─────────┘  └┘
src    └─────────┘       └─────────┘
typ    └─────────┘  └┘  └─────────┘  └┘
doc    └─────────┘        └─────────┘
465  λ y (yx : _ ≤ ε₁), le_trans yx h
id               └┘   └──────┘ └┘ 
src                    └──────┘
typ              └┘   └──────┘ └┘ 
466  
467  theorem ball_disjoint (h : ε₁ + ε₂ ≤ edist x y) : ball x ε₁ ∩ ball y ε₂ = ∅ :=
id                              └┘  └┘  └───┘      └──┘  └┘  └──┘  └┘  
src                                     └───┘        └──┘       └──┘       
typ                             └┘  └┘  └───┘      └──┘  └┘  └──┘  └┘  
doc                                                    └──┘        └──┘
468  eq_empty_iff_forall_not_mem.2 $ λ z ⟨h₁, h₂⟩,
id   └─────────────────────────┘       └┘  └┘
src  └─────────────────────────┘
typ  └─────────────────────────┘       └┘  └┘
469  not_lt_of_le (edist_triangle_left x y z)
id   └──────────┘  └─────────────────┘   
src  └──────────┘  └─────────────────┘
typ  └──────────┘  └─────────────────┘   
doc                └─────────────────┘
470    (lt_of_lt_of_le (ennreal.add_lt_add h₁ h₂) h)
id      └────────────┘  └────────────────┘        
src     └────────────┘  └────────────────┘
typ     └────────────┘  └────────────────┘        
471  
472  theorem ball_subset (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y < ⊤) : ball x ε₁ ⊆ ball y ε₂ :=
id                            └───┘    └┘  └┘        └───┘        └──┘  └┘  └──┘  └┘
src                           └───┘                    └───┘          └──┘       └──┘
typ                           └───┘    └┘  └┘        └───┘        └──┘  └┘  └──┘  └┘
doc                                                                       └──┘        └──┘
473  λ z zx, calc
id      └┘
typ     └┘
474    edist z y ≤ edist z x + edist x y : edist_triangle _ _ _
id     └───┘     └───┘    └───┘     └────────────┘
src    └───┘       └───┘      └───┘       └────────────┘
typ    └───┘     └───┘    └───┘     └────────────┘
475    ... = edist x y + edist z x : add_comm _ _
id           └───┘    └───┘     └──────┘
src          └───┘      └───┘       └──────┘
typ          └───┘    └───┘     └──────┘
476    ... < edist x y + ε₁ : (ennreal.add_lt_add_iff_left h').2 zx
id           └───┘    └┘    └─────────────────────────┘ └┘   └┘
src          └───┘            └─────────────────────────┘    
typ          └───┘    └┘    └─────────────────────────┘ └┘   └┘
477    ... ≤ ε₂ : h
id           └┘   
typ          └┘   
478  
479  theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε :=
id                                          └──┘       └┘     └──┘  └┘  └──┘  
src                                          └──┘                └──┘       └──┘
typ                                         └──┘       └┘     └──┘  └┘  └──┘  
doc                                           └──┘                  └──┘        └──┘
480  begin
st   └─────
481    have : 0 < ε - edist y x := by simpa using h,
id                 └───┘                     
src    └───────┘ └───┘  └──┘  └──────────┘
typ    └───────┘└───┘└──┘  └──────────┘
doc    └───────┘          └──┘  └──────────┘
txt    └───────┘          └──┘  └──────────┘
par    └───────┘          └──┘  └──────────┘
pid    └───┘└──┘          └──┘  └───────────┘
st   ───────────────────────────────┘└────────────┘└─
482    refine ⟨ε - edist y x, this, ball_subset _ _⟩,
id                └───┘    └──┘  └─────────┘
src    └─────┘   └───┘  └┘    └┘└─────────┘└───┘
typ    └─────┘  └───┘└┘└──┘└┘└─────────┘└───┘
doc    └─────┘          └┘    └┘           └───┘
txt    └─────┘          └┘    └┘           └───┘
par    └─────┘          └┘    └┘           └───┘
pid                    └┘    └┘           └───┘
st   ──────────────────────────────────────────────┘└─
483    { rw ennreal.add_sub_cancel_of_le (le_of_lt h), apply le_refl _},
id          └──────────────────────────┘  └──────┘          └─────┘
src      └─┘└──────────────────────────┘ └──────┘   └────┘└─────┘└┘
typ      └─┘└──────────────────────────┘ └──────┘  └────┘└─────┘└┘
doc      └─┘                                        └────┘       └┘
txt      └─┘                                        └────┘       └┘
par      └─┘                                        └────┘       └┘
pid                                                            └┘
st   ───┘└──────────────────────────────────────────┘└───────────────┘└┘
484    { have : edist y x ≠ ⊤ := lattice.ne_top_of_lt h, apply lt_top_iff_ne_top.2 this }
id              └───┘        └──────────────────┘         └───────────────┘   └──┘
src      └─────┘└───┘  └──┘└──────────────────┘   └────┘└───────────────┘└─┘    
typ      └─────┘└───┘└──┘└──────────────────┘  └────┘└───────────────┘└─┘└──┘
doc      └─────┘         └──┘                       └────┘                 └─┘    
txt      └─────┘         └──┘                       └────┘                 └─┘    
par      └─────┘         └──┘                       └────┘                 └─┘    
pid      └───┘└┘         └──┘                                             └─┘    
st   ─────────────────────────────────────────────────┘└───────────────────────────────┘└─
485  end
st   ──┘
486  
487  theorem ball_eq_empty_iff : ball x ε = ∅ ↔ ε = 0 :=
id                               └──┘       
src                              └──┘          
typ                              └──┘       
doc                              └──┘
488  eq_empty_iff_forall_not_mem.trans
id   └─────────────────────────┘└────┘
src  └─────────────────────────┘└────┘
typ  └─────────────────────────┘└────┘
489  ⟨λh, le_bot_iff.1 (le_of_not_gt (λ ε0, h _ (mem_ball_self ε0))),
id       └────────┘   └──────────┘    └┘      └───────────┘ └┘
src       └────────┘   └──────────┘             └───────────┘
typ      └────────┘   └──────────┘    └┘      └───────────┘ └┘
490  λε0 y h, not_lt_of_le (le_of_eq ε0) (pos_of_mem_ball h)⟩
id    └┘    └──────────┘  └──────┘ └┘   └─────────────┘ 
src           └──────────┘  └──────┘      └─────────────┘
typ   └┘    └──────────┘  └──────┘ └┘   └─────────────┘ 
491  
492  theorem nhds_eq : 𝓝 x = (⨅ε:{ε:ennreal // ε>0}, principal (ball x ε.val)) :=
id                             └─────┘       └───────┘  └──┘  └──┘
src                             └─────┘        └───────┘  └──┘    └──┘
typ                            └─────┘       └───────┘  └──┘  └──┘
doc                               └─────┘         └───────┘  └──┘
493  begin
st   └─────
494    rw [nhds_eq_uniformity, uniformity_edist'', lift'_infi],
id         └────────────────┘  └────────────────┘  └────────┘
src    └──┘└────────────────┘└┘└────────────────┘└┘└────────┘
typ    └──┘└────────────────┘└┘└────────────────┘└┘└────────┘
doc    └──┘                  └┘└────────────────┘└┘          
txt    └──┘                  └┘                  └┘          
par    └──┘                  └┘                  └┘          
pid      └┘                  └┘                  └┘          
st   ───────────────────────┘└──────────────────┘└──────────┘└──
495    { apply congr_arg, funext ε,
id             └───────┘
src      └────┘└───────┘  └──────┘
typ      └────┘└───────┘  └──────┘
doc      └────┘           └──────┘
txt      └────┘           └──────┘
par      └────┘           └──────┘
pid                            └┘
st   ───┘└─────────────┘└────────┘└─
496      rw [lift'_principal],
id           └─────────────┘
src      └──┘└─────────────┘
typ      └──┘└─────────────┘
doc      └──┘               
txt      └──┘               
par      └──┘               
pid        └┘               
st   ──────────────────────┘└──
497      { simp [ball, edist_comm] },
id               └──┘  └────────┘
src        └────┘└──┘└┘└────────┘└┘
typ        └────┘└──┘└┘└────────┘└┘
doc        └────┘└──┘└┘          └┘
txt        └────┘    └┘          └┘
par        └────┘    └┘          └┘
pid                └┘          
st   ─────┘└──────────────────────┘└┘
498      { exact monotone_preimage } },
id               └───────────────┘
src        └────┘└───────────────┘
typ        └────┘└───────────────┘
doc        └────┘                 
txt        └────┘                 
par        └────┘                 
pid                              
st   ─────────────────────────────┘└──┘
499    { exact ⟨⟨1, ennreal.zero_lt_one⟩⟩ },
id                  └─────────────────┘
src      └────┘  └─┘└─────────────────┘└─┘
typ      └────┘  └─┘└─────────────────┘└─┘
doc      └────┘  └─┘                   └─┘
txt      └────┘  └─┘                   └─┘
par      └────┘  └─┘                   └─┘
pid             └─┘                   └┘
st   ───┘└───────────────────────────────┘└┘
500    { intros, refl }
src      └────┘  └───┘
typ      └────┘  └───┘
doc      └────┘  └───┘
txt      └────┘  └───┘
par      └────┘  └───┘
pid                  
st   ─────────┘└─────┘└─
501  end
st   ──┘
502  
503  theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ε>0, ball x ε ⊆ s :=
id                                  └──┘    
src                                    └──┘     
typ                                 └──┘    
doc                                        └──┘
504  begin
st   └─────
505    rw [nhds_eq, mem_infi],
id         └─────┘  └──────┘
src    └──┘└─────┘└┘└──────┘
typ    └──┘└─────┘└┘└──────┘
doc    └──┘       └┘        
txt    └──┘       └┘        
par    └──┘       └┘        
pid      └┘       └┘        
st   ────────────┘└────────┘└──
506    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
507    { intros y z, cases y with y hy, cases z with z hz,
id                                           
src      └────────┘  └────┘ └────────┘  └────┘ └────────┘
typ      └────────┘  └────┘└────────┘  └────┘└────────┘
doc      └────────┘  └────┘ └────────┘  └────┘ └────────┘
txt      └────────┘  └────┘ └────────┘  └────┘ └────────┘
par      └────────┘  └────┘ └────────┘  └────┘ └────────┘
pid            └──┘        └────────┘        └────────┘
st   ───┘└────────┘└─────────────────┘└─────────────────┘└─
508      refine ⟨⟨min y z, lt_min hy hz⟩, _⟩,
id                └─┘    └────┘ └┘ └┘
src      └─────┘  └─┘  └┘└────┘    └───┘
typ      └─────┘  └─┘└┘└────┘└┘└┘└───┘
doc      └─────┘       └┘          └───┘
txt      └─────┘       └┘          └───┘
par      └─────┘       └┘          └───┘
pid                   └┘          └───┘
st   ──────────────────────────────────────┘└─
509      simp [ball_subset_ball, min_le_left, min_le_right, (≥)] },
id             └──────────────┘  └─────────┘  └──────────┘  
src      └────┘└──────────────┘└┘└─────────┘└┘└──────────┘└┘└──┘
typ      └────┘└──────────────┘└┘└─────────┘└┘└──────────┘└┘└──┘
doc      └────┘                └┘           └┘            └┘ └──┘
txt      └────┘                └┘           └┘            └┘ └──┘
par      └────┘                └┘           └┘            └┘ └──┘
pid                          └┘           └┘            └┘ └─┘
st   ───────────────────────────────────────────────────────────┘└┘
510    { exact ⟨⟨1, ennreal.zero_lt_one⟩⟩ }
id                  └─────────────────┘
src      └────┘  └─┘└─────────────────┘└─┘
typ      └────┘  └─┘└─────────────────┘└─┘
doc      └────┘  └─┘                   └─┘
txt      └────┘  └─┘                   └─┘
par      └────┘  └─┘                   └─┘
pid             └─┘                   └┘
st   ────────────────────────────────────┘└─
511  end
st   ──┘
512  
513  theorem is_open_iff : is_open s ↔ ∀x∈s, ∃ε>0, ball x ε ⊆ s :=
id                         └─────┘          └──┘    
src                        └─────┘              └──┘     
typ                        └─────┘          └──┘    
doc                        └─────┘                 └──┘
514  by simp [is_open_iff_nhds, mem_nhds_iff]
id            └──────────────┘  └──────────┘
src     └────┘└──────────────┘└┘└──────────┘└─
typ     └────┘└──────────────┘└┘└──────────┘└─
doc     └────┘                └┘            └─
txt     └────┘                └┘            └─
par     └────┘                └┘            └─
pid                         └┘            
st     └──────────────────────────────────────
515  
src  
typ  
doc  
txt  
par  
pid  
st   
516  theorem is_open_ball : is_open (ball x ε) :=
id                          └─────┘  └──┘  
src                         └─────┘  └──┘
typ                         └─────┘  └──┘  
doc                         └─────┘  └──┘
517  is_open_iff.2 $ λ y, exists_ball_subset_ball
id   └─────────┘        └─────────────────────┘
src  └─────────┘         └─────────────────────┘
typ  └─────────┘        └─────────────────────┘
518  
519  theorem ball_mem_nhds (x : α) {ε : ennreal} (ε0 : 0 < ε) : ball x ε ∈ 𝓝 x :=
id                                     └─────┘               └──┘     
src                                     └─────┘                └──┘      
typ                                    └─────┘               └──┘     
doc                                     └─────┘                 └──┘       
520  mem_nhds_sets is_open_ball (mem_ball_self ε0)
id   └───────────┘ └──────────┘  └───────────┘ └┘
src  └───────────┘ └──────────┘  └───────────┘
typ  └───────────┘ └──────────┘  └───────────┘ └┘
521  
522  /-- ε-characterization of the closure in emetric spaces -/
523  theorem mem_closure_iff' :
524    x ∈ closure s ↔ ∀ε>0, ∃y ∈ s, edist x y < ε :=
id       └─────┘            └───┘    
src       └─────┘                └───┘     
typ      └─────┘            └───┘    
doc        └─────┘
525  ⟨begin
st    └─────
526    intros hx ε hε,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid          └──────┘
st   ───────────────┘└─
527    obtain ⟨y, hy⟩ : (ball x ε ∩ s).nonempty,
id                       └──┘    
src    └───────────────┘ └──┘   └────────┘
typ    └───────────────┘ └──┘└────────┘
doc    └───────────────┘ └──┘    └────────┘
txt    └───────────────┘         └────────┘
par    └───────────────┘         └────────┘
pid          └─────────┘         └───────┘
st   ─────────────────────────────────────────┘└─
528      from mem_closure_iff.1 hx _ is_open_ball (mem_ball_self hε),
id            └─────────────┘   └┘   └──────────┘  └───────────┘ └┘
src      └───┘└─────────────┘└─┘  └─┘└──────────┘ └───────────┘  
typ      └───┘└─────────────┘└─┘└┘└─┘└──────────┘ └───────────┘└┘
doc      └───┘               └─┘  └─┘                            
txt      └───┘               └─┘  └─┘                            
par      └───┘               └─┘  └─┘                            
pid      └───┘               └─┘  └─┘                            
st   ──────────────────────────────────────────────────────────────┘└─
529    simp,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
530    exact ⟨y, ⟨hy.2, by have B := hy.1; simpa [mem_ball'] using B⟩⟩
id               └┘                 └┘           └───────┘        
src    └────┘  └┘   └──┘  └────────┘  └┘└┘└─────┘└───────┘└──────┘ └─┘
typ    └────┘ └┘ └┘└──┘  └────────┘└┘└┘└┘└─────┘└───────┘└──────┘└─┘
doc    └────┘  └┘   └──┘  └────────┘  └┘└┘└─────┘         └──────┘ └─┘
txt    └────┘  └┘   └──┘  └────────┘  └┘└┘└─────┘         └──────┘ └─┘
par    └────┘  └┘   └──┘  └────────┘  └┘└┘└─────┘         └──────┘ └─┘
pid           └┘   └──┘  └─────────┘  └─────────┘         └──────┘ └┘
st   ────────────────────┘└────────────────────────────────────────┘└─┘
531  end,
st   └─┘
532  begin
st   └─────
533    intros H,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          └┘
st   ─────────┘└─
534    apply mem_closure_iff.2,
id           └─────────────┘
src    └────┘└─────────────┘└┘
typ    └────┘└─────────────┘└┘
doc    └────┘               └┘
txt    └────┘               └┘
par    └────┘               └┘
pid                        └┘
st   ────────────────────────┘└─
535    intros o ho xo,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid          └──────┘
st   ───────────────┘└─
536    rcases is_open_iff.1 ho x xo with ⟨ε, ⟨εpos, hε⟩⟩,
id            └─────────┘   └┘  └┘
src    └─────┘└─────────┘└─┘     └───────────────────┘
typ    └─────┘└─────────┘└─┘└┘└┘└───────────────────┘
doc    └─────┘           └─┘     └───────────────────┘
txt    └─────┘           └─┘     └───────────────────┘
par    └─────┘           └─┘     └───────────────────┘
pid                     └─┘     └───────────────────┘
st   ──────────────────────────────────────────────────┘└─
537    rcases H ε εpos with ⟨y, ⟨ys, ydist⟩⟩,
id              └──┘
src    └─────┘      └────────────────────┘
typ    └─────┘└──┘└────────────────────┘
doc    └─────┘      └────────────────────┘
txt    └─────┘      └────────────────────┘
par    └─────┘      └────────────────────┘
pid                └────────────────────┘
st   ──────────────────────────────────────┘└─
538    have B : y ∈ o ∩ s := ⟨hε (by simpa [edist_comm]), ys⟩,
id                        └┘            └────────┘    └┘
src    └───────┘    └──┘      └─────┘└────────┘└─┘  
typ    └───────┘ └──┘ └┘   └─────┘└────────┘└─┘└┘
doc    └───────┘     └──┘      └─────┘          └─┘  
txt    └───────┘     └──┘      └─────┘          └─┘  
par    └───────┘     └──┘      └─────┘          └─┘  
pid    └────┘└─┘     └──┘      └──────┘          └──┘  
st   ──────────────────────────────┘└─────────────────┘└────┘└─
539    exact ⟨y, B⟩
id              
src    └────┘  └┘ └┘
typ    └────┘ └┘└┘
doc    └────┘  └┘ └┘
txt    └────┘  └┘ └┘
par    └────┘  └┘ └┘
pid           └┘ 
st   ──────────────┘
540  end⟩
st   └─┘
541  
542  theorem tendsto_nhds {f : filter β} {u : β → α} {a : α} :
id                             └────┘                  
src                            └────┘
typ                            └────┘                  
543    tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∃ n ∈ f, ∀x ∈ n, edist (u x) a < ε :=
id     └─────┘                           └───┘       
src    └─────┘                                   └───┘         
typ    └─────┘                           └───┘       
doc    └─────┘      
544  ⟨λ H ε ε0, ⟨u⁻¹' (ball a ε), H (ball_mem_nhds _ ε0), by simp⟩,
id        └┘   └─┘  └──┘       └───────────┘   └┘
src               └─┘  └──┘          └───────────┘           └──┘
typ       └┘   └─┘  └──┘       └───────────┘   └┘      └──┘
doc               └─┘  └──┘                                  └──┘
txt                                                          └──┘
par                                                          └──┘
st                                                          └───┘
545   λ H s hs,
id        └┘
typ       └┘
546    let ⟨ε, ε0, hε⟩ := mem_nhds_iff.1 hs, ⟨δ, δ0, hδ⟩ := H _ ε0 in
id     └─┘     └┘  └┘     └──────────┘  └┘      └┘  └┘     
src                       └──────────┘
typ    └─┘     └┘  └┘     └──────────┘  └┘      └┘  └┘     
547    f.sets_of_superset δ0 (λx xδ, hε (hδ x xδ))⟩
id     └───────────────┘       └┘          └┘
src     └───────────────┘
typ    └───────────────┘       └┘          └┘
548  
549  theorem tendsto_at_top [inhabited β] [semilattice_sup β] (u : β → α) {a : α} :
id                           └───────┘    └─────────────┘                  
src                          └───────┘     └─────────────┘
typ                          └───────┘    └─────────────┘                  
doc                                        └─────────────┘
550    tendsto u at_top (𝓝 a) ↔ ∀ε>0, ∃N, ∀n≥N, edist (u n) a < ε :=
id     └─────┘  └────┘                └───┘       
src    └─────┘   └────┘                    └───┘         
typ    └─────┘  └────┘                └───┘       
doc    └─────┘   └────┘  
551  begin
st   └─────
552    rw tendsto_nhds,
id        └──────────┘
src    └─┘└──────────┘
typ    └─┘└──────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────┘└─
553    apply forall_congr,
id           └──────────┘
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────┘└─
554    intro ε,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
555    apply forall_congr,
id           └──────────┘
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────┘└─
556    intro hε,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid         └─┘
st   ─────────┘└─
557    simp,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
558    exact ⟨λ ⟨s, ⟨N, hN⟩, hs⟩, ⟨N, λn hn, hs _ (hN _ hn)⟩, λ ⟨N, hN⟩, ⟨{n | n ≥ N}, ⟨⟨N, by simp⟩, hN⟩⟩⟩,
id                     └┘   └┘                                    └┘          
src    └────┘  └┘ └┘  └┘  └─┘  └─┘  └┘ └────┘  └─┘   └─┘  └──┘ └┘ └┘  └─┘ └──┘  └─┘   └┘  └──┘└─┘  └─┘
typ    └────┘  └┘ └┘ └┘└┘└─┘└┘└─┘  └┘ └────┘  └─┘   └─┘  └──┘ └┘└┘└┘└─┘ └──┘  └─┘   └┘  └──┘└─┘  └─┘
doc    └────┘  └┘ └┘  └┘  └─┘  └─┘  └┘ └────┘  └─┘   └─┘  └──┘ └┘ └┘  └─┘  └──┘   └─┘   └┘  └──┘└─┘  └─┘
txt    └────┘  └┘ └┘  └┘  └─┘  └─┘  └┘ └────┘  └─┘   └─┘  └──┘ └┘ └┘  └─┘  └──┘   └─┘   └┘  └──┘└─┘  └─┘
par    └────┘  └┘ └┘  └┘  └─┘  └─┘  └┘ └────┘  └─┘   └─┘  └──┘ └┘ └┘  └─┘  └──┘   └─┘   └┘  └──┘└─┘  └─┘
pid           └┘ └┘  └┘  └─┘  └─┘  └┘ └────┘  └─┘   └─┘  └──┘ └┘ └┘  └─┘  └──┘   └─┘   └┘  └──────┘  └─┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└───┘└──────┘└─
559  end
st   ──┘
560  
561  /-- In an emetric space, Cauchy sequences are characterized by the fact that, eventually,
562  the edistance between its elements is arbitrarily small -/
563  theorem cauchy_seq_iff [inhabited β] [semilattice_sup β] {u : β → α} :
id                           └───────┘    └─────────────┘           
src                          └───────┘     └─────────────┘
typ                          └───────┘    └─────────────┘           
doc                                        └─────────────┘
564    cauchy_seq u ↔ ∀ε>0, ∃N, ∀m n≥N, edist (u n) (u m) < ε :=
id     └────────┘              └───┘          
src    └────────┘                    └───┘             
typ    └────────┘              └───┘          
doc    └────────┘
565  begin
st   └─────
566    simp only [cauchy_seq, emetric.cauchy_iff, true_and, exists_prop, filter.mem_at_top_sets,
id                └────────┘  └────────────────┘  └──────┘  └─────────┘  └────────────────────┘
src    └─────────┘└────────┘└┘└────────────────┘└┘└──────┘└┘└─────────┘└┘└────────────────────┘└─
typ    └─────────┘└────────┘└┘└────────────────┘└┘└──────┘└┘└─────────┘└┘└────────────────────┘└─
doc    └─────────┘└────────┘└┘└────────────────┘└┘        └┘           └┘                      └─
txt    └─────────┘          └┘                  └┘        └┘           └┘                      └─
par    └─────────┘          └┘                  └┘        └┘           └┘                      └─
pid        └──┘└┘          └┘                  └┘        └┘           └┘                      └─
st   ────────────────────────────────────────────────────────────────────────────────────────────
567      filter.at_top_ne_bot, filter.mem_map, ne.def, filter.map_eq_bot_iff, not_false_iff, set.mem_set_of_eq],
id       └──────────────────┘  └────────────┘  └────┘  └───────────────────┘  └───────────┘  └───────────────┘
src  ───┘└──────────────────┘└┘└────────────┘└┘└────┘└┘└───────────────────┘└┘└───────────┘└┘└───────────────┘
typ  ───┘└──────────────────┘└┘└────────────┘└┘└────┘└┘└───────────────────┘└┘└───────────┘└┘└───────────────┘
doc  ───┘                    └┘              └┘      └┘                     └┘             └┘                 
txt  ───┘                    └┘              └┘      └┘                     └┘             └┘                 
par  ───┘                    └┘              └┘      └┘                     └┘             └┘                 
pid  ───┘                    └┘              └┘      └┘                     └┘             └┘                 
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
568    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
569    { intros H ε εpos,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid            └───────┘
st   ───┘└─────────────┘└─
570      rcases H ε εpos with ⟨t, ⟨N, hN⟩, ht⟩,
id                └──┘
src      └─────┘      └────────────────────┘
typ      └─────┘└──┘└────────────────────┘
doc      └─────┘      └────────────────────┘
txt      └─────┘      └────────────────────┘
par      └─────┘      └────────────────────┘
pid                  └────────────────────┘
st   ────────────────────────────────────────┘└─
571      exact ⟨N, λm n hm hn, ht _ _ (hN _ hn) (hN _ hm)⟩ },
id                            └┘                └┘
src      └────┘  └┘ └─────────┘  └───┘   └─┘  └┘   └─┘  └─┘
typ      └────┘ └┘ └─────────┘└┘└───┘   └─┘  └┘ └┘└─┘  └─┘
doc      └────┘  └┘ └─────────┘  └───┘   └─┘  └┘   └─┘  └─┘
txt      └────┘  └┘ └─────────┘  └───┘   └─┘  └┘   └─┘  └─┘
par      └────┘  └┘ └─────────┘  └───┘   └─┘  └┘   └─┘  └─┘
pid             └┘ └─────────┘  └───┘   └─┘  └┘   └─┘  └┘
st   ─────────────────────────────────────────────────────┘└┘
572    { intros H ε εpos,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid            └───────┘
st   ──────────────────┘└─
573      rcases H (ε/2) (ennreal.half_pos εpos) with ⟨N, hN⟩,
id                    └──────────────┘ └──┘
src      └─────┘   └─┘ └──────────────┘    └────────────┘
typ      └─────┘ └─┘ └──────────────┘└──┘└────────────┘
doc      └─────┘    └─┘                     └────────────┘
txt      └─────┘    └─┘                     └────────────┘
par      └─────┘    └─┘                     └────────────┘
pid                └─┘                     └────────────┘
st   ──────────────────────────────────────────────────────┘└─
574      existsi ball (u N) (ε/2),
id               └──┘      
src      └──────┘└──┘   └┘   └┘
typ      └──────┘└──┘ └┘  └┘
doc      └──────┘└──┘   └┘   └┘
txt      └──────┘       └┘   └┘
par      └──────┘       └┘   └┘
pid                    └┘   └┘
st   ───────────────────────────┘└─
575      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
576      { exact ⟨N, λx hx, hN _ _ (le_refl N) hx⟩ },
id                          └┘      └─────┘ 
src        └────┘  └┘ └────┘  └───┘ └─────┘ └┘  └┘
typ        └────┘  └┘ └────┘└┘└───┘ └─────┘└┘  └┘
doc        └────┘  └┘ └────┘  └───┘         └┘  └┘
txt        └────┘  └┘ └────┘  └───┘         └┘  └┘
par        └────┘  └┘ └────┘  └───┘         └┘  └┘
pid               └┘ └────┘  └───┘         └┘  
st   ─────┘└──────────────────────────────────────┘└┘
577      { exact λx y hx hy, calc
src        └────┘ └─────────┘    
typ        └────┘ └─────────┘    
doc        └────┘ └─────────┘    
txt        └────┘ └─────────┘    
par        └────┘ └─────────┘    
pid              └─────────┘    
st   ─────────────────────────────
578          edist x y ≤ edist x (u N) + edist y (u N) : edist_triangle_right _ _ _
id                                       └───┘         └──────────────────┘
src  ───────┘                 └┘ └───┘    └──┘└──────────────────┘└──────
typ  ───────┘                 └┘ └───┘  └──┘└──────────────────┘└──────
doc  ───────┘                 └┘          └──┘                    └──────
txt  ───────┘                 └┘          └──┘                    └──────
par  ───────┘                 └┘          └──┘                    └──────
pid  ───────┘                 └┘          └──┘                    └──────
st   ───────────────────────────────────────────────────────────────────────────────
579          ... < ε/2 + ε/2 : ennreal.add_lt_add hx hy
id                            └────────────────┘
src  ───────────┘   └┘  └──┘└────────────────┘    
typ  ───────────┘   └┘  └──┘└────────────────┘    
doc  ───────────┘   └┘   └──┘                      
txt  ───────────┘   └┘   └──┘                      
par  ───────────┘   └┘   └──┘                      
pid  ───────────┘   └┘   └──┘                      
st   ───────────────────────────────────────────────────
580          ... = ε : ennreal.add_halves _ } }
id                    └────────────────┘
src  ───────────┘  └─┘└────────────────┘└─┘
typ  ───────────┘ └─┘└────────────────┘└─┘
doc  ───────────┘  └─┘                  └─┘
txt  ───────────┘  └─┘                  └─┘
par  ───────────┘  └─┘                  └─┘
pid  ───────────┘  └─┘                  └┘
st   ──────────────────────────────────────┘└───
581  end
st   ──┘
582  
583  /-- A variation around the emetric characterization of Cauchy sequences -/
584  theorem cauchy_seq_iff' [inhabited β] [semilattice_sup β] {u : β → α} :
id                            └───────┘    └─────────────┘           
src                           └───────┘     └─────────────┘
typ                           └───────┘    └─────────────┘           
doc                                         └─────────────┘
585    cauchy_seq u ↔ ∀ε>(0 : ennreal), ∃N, ∀n≥N, edist (u n) (u N) < ε :=
id     └────────┘          └─────┘        └───┘          
src    └────────┘            └─────┘           └───┘             
typ    └────────┘          └─────┘        └───┘          
doc    └────────┘             └─────┘
586  begin
st   └─────
587    rw cauchy_seq_iff,
id        └────────────┘
src    └─┘└────────────┘
typ    └─┘└────────────┘
doc    └─┘└────────────┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────┘└─
588    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
589    { intros H ε εpos,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid            └───────┘
st   ───┘└─────────────┘└─
590      rcases H ε εpos with ⟨N, hN⟩,
id                └──┘
src      └─────┘      └───────────┘
typ      └─────┘└──┘└───────────┘
doc      └─────┘      └───────────┘
txt      └─────┘      └───────────┘
par      └─────┘      └───────────┘
pid                  └───────────┘
st   ───────────────────────────────┘└─
591      exact ⟨N, λn hn, hN _ _ (le_refl N) hn⟩ },
id                        └┘      └─────┘ 
src      └────┘  └┘ └────┘  └───┘ └─────┘ └┘  └┘
typ      └────┘  └┘ └────┘└┘└───┘ └─────┘└┘  └┘
doc      └────┘  └┘ └────┘  └───┘         └┘  └┘
txt      └────┘  └┘ └────┘  └───┘         └┘  └┘
par      └────┘  └┘ └────┘  └───┘         └┘  └┘
pid             └┘ └────┘  └───┘         └┘  
st   ───────────────────────────────────────────┘└┘
592    { intros H ε εpos,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid            └───────┘
st   ──────────────────┘└─
593      rcases H (ε/2) (ennreal.half_pos εpos) with ⟨N, hN⟩,
id                    └──────────────┘ └──┘
src      └─────┘   └─┘ └──────────────┘    └────────────┘
typ      └─────┘ └─┘ └──────────────┘└──┘└────────────┘
doc      └─────┘    └─┘                     └────────────┘
txt      └─────┘    └─┘                     └────────────┘
par      └─────┘    └─┘                     └────────────┘
pid                └─┘                     └────────────┘
st   ──────────────────────────────────────────────────────┘└─
594      exact ⟨N, λ m n hm hn, calc
src      └────┘  └┘ └──────────┘    
typ      └────┘  └┘ └──────────┘    
doc      └────┘  └┘ └──────────┘    
txt      └────┘  └┘ └──────────┘    
par      └────┘  └┘ └──────────┘    
pid             └┘ └──────────┘    
st   ────────────────────────────────
595         edist (u n) (u m) ≤ edist (u n) (u N) + edist (u m) (u N) : edist_triangle_right _ _ _
id                                                  └───┘             └──────────────────┘
src  ──────┘        └┘   └┘         └┘   └┘ └───┘   └┘   └──┘└──────────────────┘└──────
typ  ──────┘        └┘   └┘         └┘   └┘ └───┘   └┘ └──┘└──────────────────┘└──────
doc  ──────┘        └┘   └┘         └┘   └┘         └┘   └──┘                    └──────
txt  ──────┘        └┘   └┘         └┘   └┘         └┘   └──┘                    └──────
par  ──────┘        └┘   └┘         └┘   └┘         └┘   └──┘                    └──────
pid  ──────┘        └┘   └┘         └┘   └┘         └┘   └──┘                    └──────
st   ──────────────────────────────────────────────────────────────────────────────────────────────
596                      ... < ε/2 + ε/2 : ennreal.add_lt_add (hN _ hn) (hN _ hm)
id                                        └────────────────┘            └┘
src  ───────────────────────┘   └┘  └──┘└────────────────┘   └─┘  └┘   └─┘  └─
typ  ───────────────────────┘   └┘  └──┘└────────────────┘   └─┘  └┘ └┘└─┘  └─
doc  ───────────────────────┘   └┘   └──┘                     └─┘  └┘   └─┘  └─
txt  ───────────────────────┘   └┘   └──┘                     └─┘  └┘   └─┘  └─
par  ───────────────────────┘   └┘   └──┘                     └─┘  └┘   └─┘  └─
pid  ───────────────────────┘   └┘   └──┘                     └─┘  └┘   └─┘  └─
st   ─────────────────────────────────────────────────────────────────────────────
597                      ... = ε : ennreal.add_halves _⟩ }
id                                └────────────────┘
src  ───────────────────────┘  └─┘└────────────────┘└──┘
typ  ───────────────────────┘ └─┘└────────────────┘└──┘
doc  ───────────────────────┘  └─┘                  └──┘
txt  ───────────────────────┘  └─┘                  └──┘
par  ───────────────────────┘  └─┘                  └──┘
pid  ───────────────────────┘  └─┘                  └─┘
st   ───────────────────────────────────────────────────┘└─
598  end
st   ──┘
599  
600  /-- A variation of the emetric characterization of Cauchy sequences that deals with
601  `nnreal` upper bounds. -/
602  theorem cauchy_seq_iff_nnreal [inhabited β] [semilattice_sup β] {u : β → α} :
id                                  └───────┘    └─────────────┘           
src                                 └───────┘     └─────────────┘
typ                                 └───────┘    └─────────────┘           
doc                                               └─────────────┘
603    cauchy_seq u ↔ ∀ ε : nnreal, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u N) (u n) < ε :=
id     └────────┘         └────┘                   └───┘          
src    └────────┘          └────┘                        └───┘             
typ    └────────┘         └────┘                   └───┘          
doc    └────────┘           └────┘
604  begin
st   └─────
605    refine cauchy_seq_iff'.trans
id            └───────────────────┘
src    └─────┘└───────────────────┘
typ    └─────┘└───────────────────┘
doc    └─────┘└───────────────────┘
txt    └─────┘                     
par    └─────┘                     
pid                               
st   ───────────────────────────────
606      ⟨λ H ε εpos, (H ε (ennreal.coe_pos.2 εpos)).imp $
id                          └─────────────┘
src  ───┘  └─────────┘    └─────────────┘└─┘    └─────┘ 
typ  ───┘  └─────────┘    └─────────────┘└─┘    └─────┘ 
doc  ───┘  └─────────┘                   └─┘    └─────┘ 
txt  ───┘  └─────────┘                   └─┘    └─────┘ 
par  ───┘  └─────────┘                   └─┘    └─────┘ 
pid  ───┘  └─────────┘                   └─┘    └─────┘ 
st   ──────────────────────────────────────────────────────
607        λ N hN n hn, edist_comm (u n) (u N) ▸ hN n hn,
id                      └────────┘            
src  ─────┘ └──────────┘└────────┘   └┘   └┘     └─
typ  ─────┘ └──────────┘└────────┘   └┘  └┘     └─
doc  ─────┘ └──────────┘             └┘   └┘      └─
txt  ─────┘ └──────────┘             └┘   └┘      └─
par  ─────┘ └──────────┘             └┘   └┘      └─
pid  ─────┘ └──────────┘             └┘   └┘      └─
st   ─────────────────────────────────────────────────────
608        λ H ε εpos, _⟩,
src  ─────┘ └───────────┘
typ  ─────┘ └───────────┘
doc  ─────┘ └───────────┘
txt  ─────┘ └───────────┘
par  ─────┘ └───────────┘
pid  ─────┘ └───────────┘
st   ───────────────────┘└─
609    specialize H ((min 1 ε).to_nnreal)
id                   └─┘   
src    └─────────┘   └─┘└─┘ └────────────
typ    └─────────┘  └─┘└─┘└────────────
doc    └─────────┘      └─┘ └────────────
txt    └─────────┘      └─┘ └────────────
par    └─────────┘      └─┘ └────────────
pid                    └─┘ └────────────
st   ─────────────────────────────────────
610      (ennreal.to_nnreal_pos_iff.2 ⟨lt_min ennreal.zero_lt_one εpos,
id        └───────────────────────┘    └────┘ └─────────────────┘ └──┘
src  ───┘ └───────────────────────┘└─┘ └────┘└─────────────────┘    └─
typ  ───┘ └───────────────────────┘└─┘ └────┘└─────────────────┘└──┘└─
doc  ───┘                          └─┘                              └─
txt  ───┘                          └─┘                              └─
par  ───┘                          └─┘                              └─
pid  ───┘                          └─┘                              └─
st   ───────────────────────────────────────────────────────────────────
611        ennreal.lt_top_iff_ne_top.1 $ min_lt_iff.2 $ or.inl ennreal.coe_lt_top⟩),
id         └───────────────────────┘     └────────┘     └────┘ └────────────────┘
src  ─────┘└───────────────────────┘└─┘ └────────┘└─┘ └────┘└────────────────┘└┘
typ  ─────┘└───────────────────────┘└─┘ └────────┘└─┘ └────┘└────────────────┘└┘
doc  ─────┘                         └─┘           └─┘                         └┘
txt  ─────┘                         └─┘           └─┘                         └┘
par  ─────┘                         └─┘           └─┘                         └┘
pid  ─────┘                         └─┘           └─┘                         └┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
612    refine H.imp (λ N hN n hn, edist_comm (u N) (u n) ▸ lt_of_lt_of_le (hN n hn) _),
id            └───┘               └────────┘              └────────────┘
src    └─────┘└───┘  └──────────┘└────────┘   └┘   └┘ └────────────┘      └──┘
typ    └─────┘└───┘  └──────────┘└────────┘   └┘  └┘ └────────────┘      └──┘
doc    └─────┘       └──────────┘             └┘   └┘                     └──┘
txt    └─────┘       └──────────┘             └┘   └┘                     └──┘
par    └─────┘       └──────────┘             └┘   └┘                     └──┘
pid                 └──────────┘             └┘   └┘                     └──┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
613    refine ennreal.coe_le_iff.2 _,
id            └────────────────┘
src    └─────┘└────────────────┘└──┘
typ    └─────┘└────────────────┘└──┘
doc    └─────┘                  └──┘
txt    └─────┘                  └──┘
par    └─────┘                  └──┘
pid                            └──┘
st   ──────────────────────────────┘└─
614    rintros ε rfl,
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid           └────┘
st   ──────────────┘└─
615    rw [← ennreal.coe_one, ← ennreal.coe_min, ennreal.to_nnreal_coe],
id           └─────────────┘    └─────────────┘  └───────────────────┘
src    └────┘└─────────────┘└──┘└─────────────┘└┘└───────────────────┘
typ    └────┘└─────────────┘└──┘└─────────────┘└┘└───────────────────┘
doc    └────┘               └──┘               └┘                     
txt    └────┘               └──┘               └┘                     
par    └────┘               └──┘               └┘                     
pid      └──┘               └──┘               └┘                     
st   ──────────────────────┘└─────────────────┘└─────────────────────┘└──
616    apply min_le_right
id           └──────────┘
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘            
txt    └────┘            
par    └────┘            
pid                     
st   ────────────────────┘
617  end
st   └─┘
618  
619  theorem totally_bounded_iff {s : set α} :
id                                    └─┘ 
src                                   └─┘
typ                                   └─┘ 
620    totally_bounded s ↔ ∀ ε > 0, ∃t : set α, finite t ∧ s ⊆ ⋃y∈t, ball y ε :=
id     └─────────────┘               └─┘  └────┘       └──┘  
src    └─────────────┘                 └─┘   └────┘           └──┘
typ    └─────────────┘               └─┘  └────┘       └──┘  
doc    └─────────────┘                          └────┘             └──┘
621  ⟨λ H ε ε0, H _ (edist_mem_uniformity ε0),
id        └┘      └──────────────────┘ └┘
src                  └──────────────────┘
typ       └┘      └──────────────────┘ └┘
doc                  └──────────────────┘
622   λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru,
id        └┘  └─┘    └┘  └┘     └──────────────────┘  └┘
src                                └──────────────────┘
typ       └┘  └─┘    └┘  └┘     └──────────────────┘  └┘
doc                                └──────────────────┘
623                 ⟨t, ft, h⟩ := H ε ε0 in
id                     └┘       
typ                    └┘       
624    ⟨t, ft, subset.trans h $ Union_subset_Union $ λ y, Union_subset_Union $ λ yt z, hε⟩⟩
id             └──────────┘     └────────────────┘       └────────────────┘     └┘ 
src            └──────────┘     └────────────────┘        └────────────────┘
typ            └──────────┘     └────────────────┘       └────────────────┘     └┘ 
625  
626  theorem totally_bounded_iff' {s : set α} :
id                                     └─┘ 
src                                    └─┘
typ                                    └─┘ 
627    totally_bounded s ↔ ∀ ε > 0, ∃t⊆s, finite t ∧ s ⊆ ⋃y∈t, ball y ε :=
id     └─────────────┘             └────┘       └──┘  
src    └─────────────┘                 └────┘           └──┘
typ    └─────────────┘             └────┘       └──┘  
doc    └─────────────┘                    └────┘             └──┘
628  ⟨λ H ε ε0, (totally_bounded_iff_subset.1 H) _ (edist_mem_uniformity ε0),
id        └┘   └────────────────────────┘       └──────────────────┘ └┘
src              └────────────────────────┘        └──────────────────┘
typ       └┘   └────────────────────────┘       └──────────────────┘ └┘
doc                                                 └──────────────────┘
629   λ H r ru, let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru,
id        └┘  └─┘    └┘  └┘     └──────────────────┘  └┘
src                                └──────────────────┘
typ       └┘  └─┘    └┘  └┘     └──────────────────┘  └┘
doc                                └──────────────────┘
630                 ⟨t, _, ft, h⟩ := H ε ε0 in
id                        └┘       
typ                       └┘       
631    ⟨t, ft, subset.trans h $ Union_subset_Union $ λ y, Union_subset_Union $ λ yt z, hε⟩⟩
id             └──────────┘     └────────────────┘       └────────────────┘     └┘ 
src            └──────────┘     └────────────────┘        └────────────────┘
typ            └──────────┘     └────────────────┘       └────────────────┘     └┘ 
632  
633  section compact
634  
635  /-- A compact set in an emetric space is separable, i.e., it is the closure of a countable set -/
636  lemma countable_closure_of_compact {α : Type u} [emetric_space α] {s : set α} (hs : compact s) :
id                                                    └───────────┘        └─┘         └─────┘ 
src                                                   └───────────┘         └─┘          └─────┘
typ                                                   └───────────┘        └─┘         └─────┘ 
doc                                                   └───────────┘                      └─────┘
637    ∃ t ⊆ s, (countable t ∧ s = closure t) :=
id           └───────┘     └─────┘ 
src            └───────┘       └─────┘
typ          └───────┘     └─────┘ 
doc              └───────┘         └─────┘
638  begin
st   └─────
639    have A : ∀ (e:ennreal), e > 0 → ∃ t ⊆ s, (finite t ∧ s ⊆ (⋃x∈t, ball x e)) :=
id                   └─────┘                  └────┘             └──┘
src    └───────┘ └──┘└─────┘  └─┘ └───┘  └────┘     └┘ └──┘  └─────
typ    └───────┘ └──┘└─────┘  └─┘ └───┘  └────┘    └┘ └──┘  └─────
doc    └───────┘ └──┘└─────┘   └─┘  └───┘   └────┘     └┘ └──┘  └─────
txt    └───────┘ └──┘          └─┘  └───┘               └┘        └─────
par    └───────┘ └──┘          └─┘  └───┘               └┘        └─────
pid    └────┘└─┘ └──┘          └─┘  └───┘               └┘        └┘└───
st   ────────────────────────────────────────────────────────────────────────────────
640      totally_bounded_iff'.1 (compact_iff_totally_bounded_complete.1 hs).1,
id       └──────────────────┘    └──────────────────────────────────┘   └┘
src  ───┘└──────────────────┘└─┘ └──────────────────────────────────┘└─┘  └─┘
typ  ───┘└──────────────────┘└─┘ └──────────────────────────────────┘└─┘└┘└─┘
doc  ───┘                    └─┘                                     └─┘  └─┘
txt  ───┘                    └─┘                                     └─┘  └─┘
par  ───┘                    └─┘                                     └─┘  └─┘
pid  ───┘                    └─┘                                     └─┘  └┘
st   ───────────────────────────────────────────────────────────────────────┘└─
641  --    assume e, finite_cover_balls_of_compact hs,
st   ──────────────────────────────────────────────────
642    have B : ∀ (e:ennreal), ∃ t ⊆ s, finite t ∧ (e > 0 → s ⊆ (⋃x∈t, ball x e)),
id                   └─────┘          └────┘                     └──┘
src    └───────┘ └──┘└─────┘ └───┘ └────┘     └─┘    └┘ └──┘  └┘
typ    └───────┘ └──┘└─────┘ └───┘ └────┘    └─┘   └┘ └──┘  └┘
doc    └───────┘ └──┘└─────┘  └───┘  └────┘     └─┘    └┘ └──┘  └┘
txt    └───────┘ └──┘         └───┘             └─┘     └┘        └┘
par    └───────┘ └──┘         └───┘             └─┘     └┘        └┘
pid    └────┘└─┘ └──┘         └───┘             └─┘     └┘        └┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
643    { intro e,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ───┘└─────┘└─
644      cases le_or_gt e 0 with h,
id             └──────┘ 
src      └────┘└──────┘ └───────┘
typ      └────┘└──────┘└───────┘
doc      └────┘         └───────┘
txt      └────┘         └───────┘
par      └────┘         └───────┘
pid                    └──────┘
st   ────────────────────────────┘└─
645      { exact ⟨∅, by finish⟩ },
id                
src        └────┘ └┘  └────┘└┘
typ        └────┘ └┘  └────┘└┘
doc        └────┘  └┘  └────┘└┘
txt        └────┘  └┘  └────┘└┘
par        └────┘  └┘  └────┘└┘
pid               └┘  └──────┘
st   ─────┘└──────────┘└─────┘└┘└┘
646      { rcases A e h with ⟨s, ⟨finite_s, closure_s⟩⟩, existsi s, finish }},
id                                                            
src        └─────┘   └──────────────────────────────┘  └──────┘   └─────┘
typ        └─────┘└──────────────────────────────┘  └──────┘  └─────┘
doc        └─────┘   └──────────────────────────────┘  └──────┘   └─────┘
txt        └─────┘   └──────────────────────────────┘  └──────┘   └─────┘
par        └─────┘   └──────────────────────────────┘  └──────┘   └─────┘
pid                 └──────────────────────────────┘                  
st   ─────────────────────────────────────────────────┘└─────────┘└───────┘└─┘
647    /-The desired countable set is obtained by taking for each `n` the centers of a finite cover
st   ───────────────────────────────────────────────────────────────────────────────────────────────
648    by balls of radius `1/n`, and then the union over `n`. -/
st   ────────────────────────────────────────────────────────────
649    choose T T_in_s finite_T using B,
id                                    
src    └─────────────────────────────┘
typ    └─────────────────────────────┘
doc    └─────────────────────────────┘
txt    └─────────────────────────────┘
par    └─────────────────────────────┘
pid          └┘└──────────────┘└─────┘
st   ─────────────────────────────────┘└─
650    let t := ⋃n:ℕ, T n⁻¹,
id                    └┘
src    └───────┘└┘   └┘
typ    └───────┘└┘  └┘
doc    └───────┘└┘  
txt    └───────┘ └┘   
par    └───────┘ └┘   
pid    └───┘└─┘ └┘   
st   ─────────────────────┘└─
651    have T₁ : t ⊆ s := begin apply Union_subset, assume n, apply T_in_s end,
id                                  └──────────┘
src    └────────┘   └──┘     └────┘└──────────┘└┘└──────┘└┘└────┘      └─┘
typ    └────────┘ └──┘     └────┘└──────────┘└┘└──────┘└┘└────┘      └─┘
doc    └────────┘   └──┘     └────┘            └┘└──────┘└┘└────┘      └─┘
txt    └────────┘   └──┘     └────┘            └┘└──────┘└┘└────┘      └─┘
par    └────────┘   └──┘     └────┘            └┘└──────┘└┘└────┘      └─┘
pid    └─────┘└─┘   └──┘     └─────┘            └────────────────┘      └──┘
st   ────────────────────┘└──────────────────────┘└────────┘└─────────────┘└─┘└─
652    have T₂ : countable t := by finish [countable_Union, countable_finite],
id               └───────┘                └─────────────┘  └──────────────┘
src    └────────┘└───────┘ └──┘  └──────┘└─────────────┘└┘└──────────────┘
typ    └────────┘└───────┘└──┘  └──────┘└─────────────┘└┘└──────────────┘
doc    └────────┘└───────┘ └──┘  └──────┘               └┘                
txt    └────────┘          └──┘  └──────┘               └┘                
par    └────────┘          └──┘  └──────┘               └┘                
pid    └─────┘└─┘          └──┘  └───────┘               └┘                
st   ────────────────────────────┘└─────────────────────────────────────────┘└─
653    have T₃ : s ⊆ closure t,
id                  └─────┘ 
src    └────────┘  └─────┘
typ    └────────┘ └─────┘
doc    └────────┘  └─────┘
txt    └────────┘         
par    └────────┘         
pid    └─────┘└─┘         
st   ────────────────────────┘└─
654    { intros x x_in_s,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid            └───────┘
st   ───┘└─────────────┘└─
655      apply mem_closure_iff'.2,
id             └──────────────┘
src      └────┘└──────────────┘└┘
typ      └────┘└──────────────┘└┘
doc      └────┘└──────────────┘└┘
txt      └────┘                └┘
par      └────┘                └┘
pid                           └┘
st   ───────────────────────────┘└─
656      intros ε εpos,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid            └─────┘
st   ────────────────┘└─
657      rcases ennreal.exists_inv_nat_lt (bot_lt_iff_ne_bot.1 εpos) with ⟨n, hn⟩,
id              └───────────────────────┘  └───────────────┘   └──┘
src      └─────┘└───────────────────────┘ └───────────────┘└─┘    └────────────┘
typ      └─────┘└───────────────────────┘ └───────────────┘└─┘└──┘└────────────┘
doc      └─────┘                                           └─┘    └────────────┘
txt      └─────┘                                           └─┘    └────────────┘
par      └─────┘                                           └─┘    └────────────┘
pid                                                       └─┘    └────────────┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
658      have inv_n_pos : (0 : ennreal) < (n : ℕ)⁻¹ := by simp [ennreal.bot_lt_iff_ne_bot],
id                             └─────┘   └┘                    └───────────────────────┘
src      └───────────────┘ └──┘└─────┘└┘  └─┘   └──┘  └────┘└───────────────────────┘
typ      └───────────────┘ └──┘└─────┘└┘└┘└─┘   └──┘  └────┘└───────────────────────┘
doc      └───────────────┘ └──┘└─────┘└┘   └─┘   └──┘  └────┘                         
txt      └───────────────┘ └──┘       └┘   └─┘   └──┘  └────┘                         
par      └───────────────┘ └──┘       └┘   └─┘   └──┘  └────┘                         
pid      └────────────┘└─┘ └──┘       └┘   └─┘   └──┘  └─────┘                         
st   ───────────────────────────────────────────────────┘└───────────────────────────────┘└─
659      have C : x ∈ (⋃y∈ T (n : ℕ)⁻¹, ball y (n : ℕ)⁻¹) :=
id                                  └──┘    
src      └───────┘   └─┘   └─┘   └──┘   └─┘   └────
typ      └───────┘  └─┘  └─┘   └──┘  └─┘   └────
doc      └───────┘   └─┘   └─┘   └──┘   └─┘   └────
txt      └───────┘    └─┘   └─┘           └─┘   └────
par      └───────┘    └─┘   └─┘           └─┘   └────
pid      └────┘└─┘    └─┘   └─┘           └─┘   └───
st   ────────────────────────────────────────────────────────
660        mem_of_mem_of_subset x_in_s ((finite_T (n : ℕ)⁻¹).2 inv_n_pos),
id         └──────────────────┘ └────┘   └──────┘             └───────┘
src  ─────┘└──────────────────┘                  └─┘   └──┘         
typ  ─────┘└──────────────────┘└────┘  └──────┘ └─┘   └──┘└───────┘
doc  ─────┘                                      └─┘   └──┘         
txt  ─────┘                                      └─┘   └──┘         
par  ─────┘                                      └─┘   └──┘         
pid  ─────┘                                      └─┘   └──┘         
st   ───────────────────────────────────────────────────────────────────┘└─
661      rcases mem_Union.1 C with ⟨y, _, ⟨y_in_T, rfl⟩, Dxy⟩,
id              └───────┘   
src      └─────┘└───────┘└─┘ └──────────────────────────────┘
typ      └─────┘└───────┘└─┘└──────────────────────────────┘
doc      └─────┘         └─┘ └──────────────────────────────┘
txt      └─────┘         └─┘ └──────────────────────────────┘
par      └─────┘         └─┘ └──────────────────────────────┘
pid                     └─┘ └──────────────────────────────┘
st   ───────────────────────────────────────────────────────┘└─
662      simp at Dxy,  -- Dxy : edist x y < 1 / ↑n
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid          └────┘
st   ──────────────┘└──────────────────────────────
663      have : y ∈ t := mem_of_mem_of_subset y_in_T (by apply subset_Union (λ (n:ℕ), T (n : ℕ)⁻¹)),
id                     └──────────────────┘ └────┘           └──────────┘           
src      └─────┘   └──┘└──────────────────┘         └────┘└──────────┘  └──┘ └─┘   └─┘   
typ      └─────┘ └──┘└──────────────────┘└────┘   └────┘└──────────┘  └──┘ └─┘  └─┘   
doc      └─────┘   └──┘                             └────┘              └──┘ └─┘   └─┘   
txt      └─────┘   └──┘                             └────┘              └──┘ └─┘   └─┘   
par      └─────┘   └──┘                             └────┘              └──┘ └─┘   └─┘   
pid      └───┘└┘   └──┘                             └─────┘              └──┘ └─┘   └─┘   └┘
st   ──────────────────────────────────────────────────┘└────────────────────────────────────────┘└─
664      have : edist x y < ε := lt_trans Dxy hn,
id              └───┘         └──────┘ └─┘ └┘
src      └─────┘└───┘    └──┘└──────┘   
typ      └─────┘└───┘ └──┘└──────┘└─┘└┘
doc      └─────┘         └──┘           
txt      └─────┘         └──┘           
par      └─────┘         └──┘           
pid      └───┘└┘         └──┘           
st   ──────────────────────────────────────────┘└─
665      exact ⟨y, ‹y ∈ t›, ‹edist x y < ε›⟩ },
id                        └───┘     
src      └────┘  └┘   └┘ └───┘     └┘
typ      └────┘  └┘  └┘ └───┘  └┘
doc      └────┘  └┘   └┘           └┘
txt      └────┘  └┘     └┘           └┘
par      └────┘  └┘     └┘           └┘
pid             └┘     └┘           
st   ───────────────────────────────────────┘└┘
666    have T₄ : closure t ⊆ s := calc
id               └─────┘    
src    └────────┘└─────┘   └──┘    
typ    └────────┘└─────┘ └──┘    
doc    └────────┘└─────┘   └──┘    
txt    └────────┘          └──┘    
par    └────────┘          └──┘    
pid    └─────┘└─┘          └──┘    
st   ──────────────────────────────────
667      closure t ⊆ closure s : closure_mono T₁
id                  └─────┘     └──────────┘ └┘
src  ───┘         └─────┘ └─┘└──────────┘  
typ  ───┘        └─────┘ └─┘└──────────┘└┘
doc  ───┘         └─────┘ └─┘              
txt  ───┘                 └─┘              
par  ───┘                 └─┘              
pid  ───┘                 └─┘              
st   ────────────────────────────────────────────
668      ... = s : closure_eq_of_is_closed (closed_of_compact _ hs),
id                └─────────────────────┘  └───────────────┘   └┘
src  ───────┘  └─┘└─────────────────────┘ └───────────────┘└─┘  
typ  ───────┘ └─┘└─────────────────────┘ └───────────────┘└─┘└┘
doc  ───────┘  └─┘                                         └─┘  
txt  ───────┘  └─┘                                         └─┘  
par  ───────┘  └─┘                                         └─┘  
pid  ───────┘  └─┘                                         └─┘  
st   ─────────────────────────────────────────────────────────────┘└─
669    exact ⟨t, ⟨T₁, T₂, subset.antisymm T₃ T₄⟩⟩
id               └┘  └┘  └─────────────┘ └┘ └┘
src    └────┘  └┘   └┘  └┘└─────────────┘    └─┘
typ    └────┘ └┘ └┘└┘└┘└┘└─────────────┘└┘└┘└─┘
doc    └────┘  └┘   └┘  └┘                   └─┘
txt    └────┘  └┘   └┘  └┘                   └─┘
par    └────┘  └┘   └┘  └┘                   └─┘
pid           └┘   └┘  └┘                   └┘
st   ────────────────────────────────────────────┘
670  end
st   └─┘
671  
672  end compact
673  
674  section first_countable
675  
676  @[priority 100] -- see Note [lower instance priority]
677  instance (α : Type u) [emetric_space α] :
id                          └───────────┘ 
src                         └───────────┘
typ                         └───────────┘ 
doc                         └───────────┘
678    topological_space.first_countable_topology α :=
id     └────────────────────────────────────────┘ 
src    └────────────────────────────────────────┘
typ    └────────────────────────────────────────┘ 
doc    └────────────────────────────────────────┘
679  uniform_space.first_countable_topology uniformity_has_countable_basis
id   └────────────────────────────────────┘ └────────────────────────────┘
src  └────────────────────────────────────┘ └────────────────────────────┘
typ  └────────────────────────────────────┘ └────────────────────────────┘
680  
681  end first_countable
682  
683  section second_countable
684  open topological_space
685  
686  /-- A separable emetric space is second countable: one obtains a countable basis by taking
687  the balls centered at points in a dense subset, and with rational radii. We do not register
688  this as an instance, as there is already an instance going in the other direction
689  from second countable spaces to separable spaces, and we want to avoid loops. -/
690  lemma second_countable_of_separable (α : Type u) [emetric_space α] [separable_space α] :
id                                                     └───────────┘    └─────────────┘ 
src                                                    └───────────┘     └─────────────┘
typ                                                    └───────────┘    └─────────────┘ 
doc                                                    └───────────┘     └─────────────┘
691    second_countable_topology α :=
id     └───────────────────────┘ 
src    └───────────────────────┘
typ    └───────────────────────┘ 
doc    └───────────────────────┘
692  let ⟨S, ⟨S_countable, S_dense⟩⟩ := separable_space.exists_countable_closure_eq_univ α in
id   └─┘                               └──────────────────────────────────────────────┘ 
src                                     └──────────────────────────────────────────────┘
typ  └─┘                               └──────────────────────────────────────────────┘ 
693  ⟨⟨⋃x ∈ S, ⋃ (n : nat), {ball x (n⁻¹)},
id                └─┘  └──┘   └┘
src                └─┘  └──┘     └┘
typ               └─┘  └──┘   └┘
doc                      └──┘
694  ⟨show countable ⋃x ∈ S, ⋃ (n : nat), {ball x (n⁻¹)},
id         └───────┘            └─┘  └──┘   └┘
src        └───────┘             └─┘  └──┘     └┘
typ        └───────┘            └─┘  └──┘   └┘
doc        └───────┘                   └──┘
695  { apply countable_bUnion S_countable,
id           └──────────────┘ └─────────┘
src    └────┘└──────────────┘
typ    └────┘└──────────────┘└─────────┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   └──────────────────────────────────┘└─
696    intros a aS,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
697    apply countable_Union,
id           └─────────────┘
src    └────┘└─────────────┘
typ    └────┘└─────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────┘└─
698    simp },
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘└┘
699  show uniform_space.to_topological_space α = generate_from (⋃x ∈ S, ⋃ (n : nat), {ball x (n⁻¹)}),
id        └────────────────────────────────┘   └───────────┘             └─┘  └──┘   └┘
src       └────────────────────────────────┘    └───────────┘              └─┘  └──┘     └┘
typ       └────────────────────────────────┘   └───────────┘             └─┘  └──┘   └┘
doc                                              └───────────┘                    └──┘
700  { have A : ∀ (u : set α), (u ∈ ⋃x ∈ S, ⋃ (n : nat), ({ball x ((n : ennreal)⁻¹)} : set (set α))) → is_open u,
id                     └─┘                      └─┘                └─────┘ └┘          └─┘       └─────┘
src    └───────┘ └────┘         └──┘  └────┘└─┘ └───┘    └─┘└─────┘└┘└───┘    └─┘ └──┘ └─────┘
typ    └───────┘ └────┘└─┘     └──┘ └────┘└─┘ └───┘    └─┘└─────┘└┘└───┘    └─┘└──┘ └─────┘
doc    └───────┘ └────┘         └──┘  └────┘     └───┘    └─┘└─────┘  └───┘        └──┘ └─────┘
txt    └───────┘ └────┘         └──┘   └────┘      └───┘    └─┘         └───┘        └──┘        
par    └───────┘ └────┘         └──┘   └────┘      └───┘    └─┘         └───┘        └──┘        
pid    └────┘└─┘ └────┘         └──┘   └────┘      └───┘    └─┘         └───┘        └──┘        
st   └─────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
701    { simp only [and_imp, exists_prop, set.mem_Union, set.mem_singleton_iff, exists_imp_distrib],
id                  └─────┘  └─────────┘  └───────────┘  └───────────────────┘  └────────────────┘
src      └─────────┘└─────┘└┘└─────────┘└┘└───────────┘└┘└───────────────────┘└┘└────────────────┘
typ      └─────────┘└─────┘└┘└─────────┘└┘└───────────┘└┘└───────────────────┘└┘└────────────────┘
doc      └─────────┘       └┘           └┘             └┘                     └┘                  
txt      └─────────┘       └┘           └┘             └┘                     └┘                  
par      └─────────┘       └┘           └┘             └┘                     └┘                  
pid          └──┘└┘       └┘           └┘             └┘                     └┘                  
st   ───┘└────────────────────────────────────────────────────────────────────────────────────────┘└─
702      intros u x hx i u_ball,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid            └──────────────┘
st   ─────────────────────────┘└─
703      rw [u_ball],
id           └────┘
src      └──┘      
typ      └──┘└────┘
doc      └──┘      
txt      └──┘      
par      └──┘      
pid        └┘      
st   ─────────────┘└──
704      exact is_open_ball },
id             └──────────┘
src      └────┘└──────────┘
typ      └────┘└──────────┘
doc      └────┘            
txt      └────┘            
par      └────┘            
pid                       
st   ──────────────────────┘└┘
705    have B : is_topological_basis (⋃x ∈ S, ⋃ (n : nat), ({ball x (n⁻¹)} : set (set α))),
id              └──────────────────┘               └─┘                        └─┘ 
src    └───────┘└──────────────────┘  └──┘  └────┘└─┘ └───┘     └───┘    └─┘ └─┘
typ    └───────┘└──────────────────┘  └──┘ └────┘└─┘ └───┘     └───┘    └─┘└─┘
doc    └───────┘└──────────────────┘  └──┘  └────┘     └───┘     └───┘        └─┘
txt    └───────┘                      └──┘   └────┘      └───┘     └───┘        └─┘
par    └───────┘                      └──┘   └────┘      └───┘     └───┘        └─┘
pid    └────┘└─┘                      └──┘   └────┘      └───┘     └───┘        └─┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
706    { refine is_topological_basis_of_open_of_nhds A (λa u au open_u, _),
id              └──────────────────────────────────┘ 
src      └─────┘└──────────────────────────────────┘   └───────────────┘
typ      └─────┘└──────────────────────────────────┘  └───────────────┘
doc      └─────┘                                       └───────────────┘
txt      └─────┘                                       └───────────────┘
par      └─────┘                                       └───────────────┘
pid                                                   └───────────────┘
st   ───┘└───────────────────────────────────────────────────────────────┘└─
707      rcases is_open_iff.1 open_u a au with ⟨ε, εpos, εball⟩,
id              └─────────┘   └────┘  └┘
src      └─────┘└─────────┘└─┘         └────────────────────┘
typ      └─────┘└─────────┘└─┘└────┘└┘└────────────────────┘
doc      └─────┘           └─┘         └────────────────────┘
txt      └─────┘           └─┘         └────────────────────┘
par      └─────┘           └─┘         └────────────────────┘
pid                       └─┘         └────────────────────┘
st   ─────────────────────────────────────────────────────────┘└─
708      have : ε / 2 > 0 := ennreal.half_pos εpos,
id                        └──────────────┘ └──┘
src      └─────┘ └─┘└────┘└──────────────┘
typ      └─────┘└─┘└────┘└──────────────┘└──┘
doc      └─────┘  └─┘ └────┘                
txt      └─────┘  └─┘ └────┘                
par      └─────┘  └─┘ └────┘                
pid      └───┘└┘  └─┘ └───┘                
st   ────────────────────────────────────────────┘└─
709      /- The ball `ball a ε` is included in `u`. We need to find one of our balls `ball x (n⁻¹)`
st   ───────────────────────────────────────────────────────────────────────────────────────────────
710      containing `a` and contained in `ball a ε`. For this, we take `n` larger than `2/ε`, and
st   ─────────────────────────────────────────────────────────────────────────────────────────────
711      then `x` in `S` at distance at most `n⁻¹` of `a` -/
st   ────────────────────────────────────────────────────────
712      rcases ennreal.exists_inv_nat_lt (bot_lt_iff_ne_bot.1 (ennreal.half_pos εpos)) with ⟨n, εn⟩,
id              └───────────────────────┘  └───────────────┘    └──────────────┘ └──┘
src      └─────┘└───────────────────────┘ └───────────────┘└─┘ └──────────────┘    └─────────────┘
typ      └─────┘└───────────────────────┘ └───────────────┘└─┘ └──────────────┘└──┘└─────────────┘
doc      └─────┘                                           └─┘                     └─────────────┘
txt      └─────┘                                           └─┘                     └─────────────┘
par      └─────┘                                           └─┘                     └─────────────┘
pid                                                       └─┘                     └─────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
713      have : (0 : ennreal) < n⁻¹ := by simp [ennreal.bot_lt_iff_ne_bot],
id                   └─────┘                  └───────────────────────┘
src      └─────┘ └──┘└─────┘└┘   └──┘  └────┘└───────────────────────┘
typ      └─────┘ └──┘└─────┘└┘  └──┘  └────┘└───────────────────────┘
doc      └─────┘ └──┘└─────┘└┘    └──┘  └────┘                         
txt      └─────┘ └──┘       └┘    └──┘  └────┘                         
par      └─────┘ └──┘       └┘    └──┘  └────┘                         
pid      └───┘└┘ └──┘       └┘    └──┘  └─────┘                         
st   ───────────────────────────────────┘└───────────────────────────────┘└─
714      have : (a : α) ∈ closure (S : set α) := by rw [S_dense]; simp,
id                       └─────┘     └─┘             └─────┘
src      └─────┘  └─┘ └┘ └─────┘  └─┘└─┘ └───┘  └──┘       └┘└──┘
typ      └─────┘ └─┘ └┘ └─────┘ └─┘└─┘└───┘  └──┘└─────┘└┘└──┘
doc      └─────┘  └─┘ └┘ └─────┘  └─┘    └───┘  └──┘       └┘└──┘
txt      └─────┘  └─┘ └┘          └─┘    └───┘  └──┘       └┘└──┘
par      └─────┘  └─┘ └┘          └─┘    └───┘  └──┘       └┘└──┘
pid      └───┘└┘  └─┘ └┘          └─┘    └──┘  └───┘       └─────┘
st   ─────────────────────────────────────────────┘└──────────┘└────┘└─
715      rcases mem_closure_iff'.1 this _ ‹(0 : ennreal) <  n⁻¹› with ⟨x, xS, xdist⟩,
id              └──────────────┘   └──┘        └─────┘       
src      └─────┘└──────────────┘└─┘    └─┘ └──┘└─────┘└┘ └┘   └──────────────────┘
typ      └─────┘└──────────────┘└─┘└──┘└─┘ └──┘└─────┘└┘ └┘  └──────────────────┘
doc      └─────┘└──────────────┘└─┘    └─┘ └──┘└─────┘└┘ └┘   └──────────────────┘
txt      └─────┘                └─┘    └─┘  └──┘       └┘ └┘    └──────────────────┘
par      └─────┘                └─┘    └─┘  └──┘       └┘ └┘    └──────────────────┘
pid                            └─┘    └─┘  └──┘       └┘ └┘    └──────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
716      existsi ball x (↑n)⁻¹,
id               └──┘   
src      └──────┘└──┘   
typ      └──────┘└──┘ 
doc      └──────┘└──┘    
txt      └──────┘        
par      └──────┘        
pid                     
st   ────────────────────────┘└─
717      have I : ball x (n⁻¹) ⊆ ball a ε := λy ydist, calc
id                            └──┘  
src      └───────┘         └┘└──┘  └──┘ └───────┘    
typ      └───────┘       └┘└──┘└──┘ └───────┘    
doc      └───────┘         └┘ └──┘  └──┘ └───────┘    
txt      └───────┘         └┘       └──┘ └───────┘    
par      └───────┘         └┘       └──┘ └───────┘    
pid      └────┘└─┘         └┘       └──┘ └───────┘    
st   ───────────────────────────────────────────────────────
718        edist y a = edist a y : edist_comm _ _
id                     └───┘      └────────┘
src  ─────┘        └───┘  └─┘└────────┘└────
typ  ─────┘        └───┘ └─┘└────────┘└────
doc  ─────┘               └─┘          └────
txt  ─────┘               └─┘          └────
par  ─────┘               └─┘          └────
pid  ─────┘               └─┘          └────
st   ─────────────────────────────────────────────
719        ... ≤ edist a x + edist y x : edist_triangle_right _ _ _
id                                      └──────────────────┘
src  ─────────┘                └─┘└──────────────────┘└──────
typ  ─────────┘               └─┘└──────────────────┘└──────
doc  ─────────┘                └─┘                    └──────
txt  ─────────┘                └─┘                    └──────
par  ─────────┘                └─┘                    └──────
pid  ─────────┘                └─┘                    └──────
st   ───────────────────────────────────────────────────────────────
720        ... < n⁻¹ + n⁻¹ : ennreal.add_lt_add xdist ydist
id                                             └───┘
src  ─────────┘        └─┘                            
typ  ─────────┘       └─┘                  └───┘     
doc  ─────────┘        └─┘                            
txt  ─────────┘        └─┘                            
par  ─────────┘        └─┘                            
pid  ─────────┘        └─┘                            
st   ───────────────────────────────────────────────────────
721        ... < ε/2 + ε/2 : ennreal.add_lt_add εn εn
id                          └────────────────┘    └┘
src  ─────────┘   └┘  └──┘└────────────────┘    
typ  ─────────┘   └┘  └──┘└────────────────┘  └┘
doc  ─────────┘   └┘   └──┘                      
txt  ─────────┘   └┘   └──┘                      
par  ─────────┘   └┘   └──┘                      
pid  ─────────┘   └┘   └──┘                      
st   ─────────────────────────────────────────────────
722        ... = ε : ennreal.add_halves _,
id                  └────────────────┘
src  ─────────┘  └─┘└────────────────┘└┘
typ  ─────────┘ └─┘└────────────────┘└┘
doc  ─────────┘  └─┘                  └┘
txt  ─────────┘  └─┘                  └┘
par  ─────────┘  └─┘                  └┘
pid  ─────────┘  └─┘                  └┘
st   ───────────────────────────────────┘└─
723      simp only [emetric.mem_ball, exists_prop, set.mem_Union, set.mem_singleton_iff],
id                  └──────────────┘  └─────────┘  └───────────┘  └───────────────────┘
src      └─────────┘└──────────────┘└┘└─────────┘└┘└───────────┘└┘└───────────────────┘
typ      └─────────┘└──────────────┘└┘└─────────┘└┘└───────────┘└┘└───────────────────┘
doc      └─────────┘                └┘           └┘             └┘                     
txt      └─────────┘                └┘           └┘             └┘                     
par      └─────────┘                └┘           └┘             └┘                     
pid          └──┘└┘                └┘           └┘             └┘                     
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
724      exact ⟨⟨x, ⟨xS, ⟨n, rfl⟩⟩⟩, ⟨by simpa, subset.trans I εball⟩⟩ },
id                  └┘     └─┘                └──────────┘  └───┘
src      └────┘   └┘   └┘  └┘└─┘└───┘   └───┘└┘└──────────┘      └─┘
typ      └────┘  └┘ └┘└┘ └┘└─┘└───┘   └───┘└┘└──────────┘└───┘└─┘
doc      └────┘   └┘   └┘  └┘   └───┘   └───┘└┘                  └─┘
txt      └────┘   └┘   └┘  └┘   └───┘   └───┘└┘                  └─┘
par      └────┘   └┘   └┘  └┘   └───┘   └───┘└┘                  └─┘
pid              └┘   └┘  └┘   └───┘   └──────┘                  └┘
st   ──────────────────────────────────┘└────┘└───────────────────────┘└┘
725    exact B.2.2 }⟩⟩⟩
id           
src    └────┘ └───┘
typ    └────┘└───┘
doc    └────┘ └───┘
txt    └────┘ └───┘
par    └────┘ └───┘
pid          └┘└─┘
st   ─────────────┘└┘
726  
727  end second_countable
728  
729  section diam
730  
731  /-- The diameter of a set in an emetric space, named `emetric.diam` -/
732  def diam (s : set α) := ⨆ (x ∈ s) (y ∈ s), edist x y
id                 └─┘                   └───┘  
src                └─┘                        └───┘
typ                └─┘                   └───┘  
doc                                          
733  
734  lemma diam_le_iff_forall_edist_le {d : ennreal} :
id                                          └─────┘
src                                         └─────┘
typ                                         └─────┘
doc                                         └─────┘
735    diam s ≤ d ↔ ∀ (x ∈ s) (y ∈ s), edist x y ≤ d :=
id     └──┘                   └───┘    
src    └──┘                          └───┘     
typ    └──┘                   └───┘    
doc    └──┘
736  by simp only [diam, supr_le_iff]
id                 └──┘  └─────────┘
src     └─────────┘└──┘└┘└─────────┘└─
typ     └─────────┘└──┘└┘└─────────┘└─
doc     └─────────┘└──┘└┘           └─
txt     └─────────┘    └┘           └─
par     └─────────┘    └┘           └─
pid         └──┘└┘    └┘           
st     └──────────────────────────────
737  
src  
typ  
doc  
txt  
par  
pid  
st   
738  /-- If two points belong to some set, their edistance is bounded by the diameter of the set -/
739  lemma edist_le_diam_of_mem (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ diam s :=
id                                                    └───┘    └──┘ 
src                                                       └───┘      └──┘
typ                                                   └───┘    └──┘ 
doc                                                                     └──┘
740  diam_le_iff_forall_edist_le.1 (le_refl _) x hx y hy
id   └─────────────────────────┘   └─────┘     └┘  └┘
src  └─────────────────────────┘   └─────┘
typ  └─────────────────────────┘   └─────┘     └┘  └┘
741  
742  /-- If the distance between any two points in a set is bounded by some constant, this constant
743  bounds the diameter. -/
744  lemma diam_le_of_forall_edist_le {d : ennreal} (h : ∀ (x ∈ s) (y ∈ s), edist x y ≤ d) :
id                                         └─────┘                     └───┘    
src                                        └─────┘                          └───┘     
typ                                        └─────┘                     └───┘    
doc                                        └─────┘
745    diam s ≤ d :=
id     └──┘   
src    └──┘   
typ    └──┘   
doc    └──┘
746  diam_le_iff_forall_edist_le.2 h
id   └─────────────────────────┘  
src  └─────────────────────────┘
typ  └─────────────────────────┘  
747  
748  /-- The diameter of a subsingleton vanishes. -/
749  lemma diam_subsingleton (hs : s.subsingleton) : diam s = 0 :=
id                                 └───────────┘    └──┘  
src                                 └───────────┘    └──┘   
typ                                └───────────┘    └──┘  
doc                                 └───────────┘    └──┘
750  le_zero_iff_eq.1 $ diam_le_of_forall_edist_le $
id   └────────────┘    └────────────────────────┘
src  └────────────┘    └────────────────────────┘
typ  └────────────┘    └────────────────────────┘
doc                     └────────────────────────┘
751  λ x hx y hy, (hs hx hy).symm ▸ edist_self y ▸ le_refl _
id      └┘  └┘   └┘ └┘ └┘ └──┘   └────────┘   └─────┘
src                         └──┘   └────────┘    └─────┘
typ     └┘  └┘   └┘ └┘ └┘ └──┘   └────────┘   └─────┘
752  
753  /-- The diameter of the empty set vanishes -/
754  @[simp] lemma diam_empty : diam (∅ : set α) = 0 :=
id                              └──┘     └─┘   
src                             └──┘     └─┘    
typ                             └──┘     └─┘   
doc    └──┘                     └──┘
755  diam_subsingleton subsingleton_empty
id   └───────────────┘ └────────────────┘
src  └───────────────┘ └────────────────┘
typ  └───────────────┘ └────────────────┘
doc  └───────────────┘
756  
757  /-- The diameter of a singleton vanishes -/
758  @[simp] lemma diam_singleton : diam ({x} : set α) = 0 :=
id                                  └──┘      └─┘   
src                                 └──┘       └─┘    
typ                                 └──┘      └─┘   
doc    └──┘                         └──┘
759  diam_subsingleton subsingleton_singleton
id   └───────────────┘ └────────────────────┘
src  └───────────────┘ └────────────────────┘
typ  └───────────────┘ └────────────────────┘
doc  └───────────────┘
760  
761  lemma diam_eq_zero_iff : diam s = 0 ↔ s.subsingleton :=
id                            └──┘      └───────────┘
src                           └──┘        └───────────┘
typ                           └──┘      └───────────┘
doc                           └──┘          └───────────┘
762  ⟨λ h x hx y hy, edist_le_zero.1 $ h ▸ edist_le_diam_of_mem hx hy, diam_subsingleton⟩
id        └┘  └┘  └───────────┘      └──────────────────┘ └┘ └┘  └───────────────┘
src                  └───────────┘       └──────────────────┘        └───────────────┘
typ       └┘  └┘  └───────────┘      └──────────────────┘ └┘ └┘  └───────────────┘
doc                                        └──────────────────┘        └───────────────┘
763  
764  lemma diam_pos_iff : 0 < diam s ↔ ∃ (x ∈ s) (y ∈ s), x ≠ y :=
id                           └──┘                  
src                          └──┘                       
typ                          └──┘                  
doc                           └──┘
765  begin
st   └─────
766    have := not_congr (@diam_eq_zero_iff _ _ s),
id             └───────┘   └──────────────┘     
src    └──────┘└───────┘  └──────────────┘└───┘ 
typ    └──────┘└───────┘  └──────────────┘└───┘
doc    └──────┘                           └───┘ 
txt    └──────┘                           └───┘ 
par    └──────┘                           └───┘ 
pid    └───┘└─┘                           └───┘ 
st   ────────────────────────────────────────────┘└─
767    dunfold set.subsingleton at this,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid           └───────────────┘└──────┘
st   ─────────────────────────────────┘└─
768    push_neg at this,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid            └──────┘
st   ─────────────────┘└─
769    simpa only [zero_lt_iff_ne_zero, exists_prop] using this
id                 └─────────────────┘  └─────────┘        └──┘
src    └──────────┘└─────────────────┘└┘└─────────┘└──────┘    
typ    └──────────┘└─────────────────┘└┘└─────────┘└──────┘└──┘
doc    └──────────┘                   └┘           └──────┘    
txt    └──────────┘                   └┘           └──────┘    
par    └──────────┘                   └┘           └──────┘    
pid         └──┘└┘                   └┘           └────┘    
st   ──────────────────────────────────────────────────────────┘
770  end
st   └─┘
771  
772  lemma diam_insert : diam (insert x s) = max (diam s) (⨆ y ∈ s, edist y x) :=
id                       └──┘  └────┘     └─┘  └──┘         └───┘  
src                      └──┘  └────┘       └─┘  └──┘            └───┘
typ                      └──┘  └────┘     └─┘  └──┘         └───┘  
doc                      └──┘                     └──┘           
773  eq_of_forall_ge_iff $ λ d, by simp only [diam_le_iff_forall_edist_le, ball_insert_iff, max_le_iff,
id   └─────────────────┘                     └─────────────────────────┘  └─────────────┘  └────────┘
src  └─────────────────┘           └─────────┘└─────────────────────────┘└┘└─────────────┘└┘└────────┘└─
typ  └─────────────────┘          └─────────┘└─────────────────────────┘└┘└─────────────┘└┘└────────┘└─
doc                                └─────────┘                           └┘               └┘          └─
txt                                └─────────┘                           └┘               └┘          └─
par                                └─────────┘                           └┘               └┘          └─
pid                                    └──┘└┘                           └┘               └┘          └─
st                                └─────────────────────────────────────────────────────────────────────
774    edist_self, zero_le, true_and, supr_le_iff, forall_and_distrib, edist_comm x, and_self,
id     └────────┘  └─────┘  └──────┘  └─────────┘  └────────────────┘  └────────┘   └──────┘
src  ─┘└────────┘└┘└─────┘└┘└──────┘└┘└─────────┘└┘└────────────────┘└┘└────────┘ └┘└──────┘└─
typ  ─┘└────────┘└┘└─────┘└┘└──────┘└┘└─────────┘└┘└────────────────┘└┘└────────┘└┘└──────┘└─
doc  ─┘          └┘       └┘        └┘           └┘                  └┘           └┘        └─
txt  ─┘          └┘       └┘        └┘           └┘                  └┘           └┘        └─
par  ─┘          └┘       └┘        └┘           └┘                  └┘           └┘        └─
pid  ─┘          └┘       └┘        └┘           └┘                  └┘           └┘        └─
st   ──────────────────────────────────────────────────────────────────────────────────────────
775    (and_assoc _ _).symm, max_comm (diam s)]
id      └───────┘            └──────┘  └──┘ 
src  ─┘ └───────┘└──────────┘└──────┘ └──┘ └──
typ  ─┘ └───────┘└──────────┘└──────┘ └──┘└──
doc  ─┘          └──────────┘         └──┘ └──
txt  ─┘          └──────────┘              └──
par  ─┘          └──────────┘              └──
pid  ─┘          └──────────┘              └┘
st   ───────────────────────────────────────────
776  
src  
typ  
doc  
txt  
par  
pid  
st   
777  lemma diam_pair : diam ({x, y} : set α) = edist x y :=
id                     └──┘       └─┘    └───┘  
src                    └──┘         └─┘     └───┘
typ                    └──┘       └─┘    └───┘  
doc                    └──┘
778  by simp only [set.insert_of_has_insert, supr_singleton, diam_insert, diam_singleton,
id                 └──────────────────────┘  └────────────┘  └─────────┘  └────────────┘
src     └─────────┘└──────────────────────┘└┘└────────────┘└┘└─────────┘└┘└────────────┘└─
typ     └─────────┘└──────────────────────┘└┘└────────────┘└┘└─────────┘└┘└────────────┘└─
doc     └─────────┘                        └┘              └┘           └┘└────────────┘└─
txt     └─────────┘                        └┘              └┘           └┘              └─
par     └─────────┘                        └┘              └┘           └┘              └─
pid         └──┘└┘                        └┘              └┘           └┘              └─
st     └──────────────────────────────────────────────────────────────────────────────────
779    ennreal.max_zero_left]
id     └───────────────────┘
src  ─┘└───────────────────┘└─
typ  ─┘└───────────────────┘└─
doc  ─┘                     └─
txt  ─┘                     └─
par  ─┘                     └─
pid  ─┘                     
st   ─────────────────────────
780  
src  
typ  
doc  
txt  
par  
pid  
st   
781  lemma diam_triple :
782    diam ({x, y, z} : set α) = max (edist x y) (max (edist y z) (edist x z)) :=
id     └──┘        └─┘    └─┘  └───┘     └─┘  └───┘     └───┘  
src    └──┘           └─┘     └─┘  └───┘       └─┘  └───┘       └───┘
typ    └──┘        └─┘    └─┘  └───┘     └─┘  └───┘     └───┘  
doc    └──┘
783  by simp only [set.insert_of_has_insert, diam_insert, supr_insert, supr_singleton, diam_singleton,
id                 └──────────────────────┘  └─────────┘  └─────────┘  └────────────┘  └────────────┘
src     └─────────┘└──────────────────────┘└┘└─────────┘└┘└─────────┘└┘└────────────┘└┘└────────────┘└─
typ     └─────────┘└──────────────────────┘└┘└─────────┘└┘└─────────┘└┘└────────────┘└┘└────────────┘└─
doc     └─────────┘                        └┘           └┘           └┘              └┘└────────────┘└─
txt     └─────────┘                        └┘           └┘           └┘              └┘              └─
par     └─────────┘                        └┘           └┘           └┘              └┘              └─
pid         └──┘└┘                        └┘           └┘           └┘              └┘              └─
st     └───────────────────────────────────────────────────────────────────────────────────────────────
784    ennreal.max_zero_left, ennreal.sup_eq_max]
id     └───────────────────┘  └────────────────┘
src  ─┘└───────────────────┘└┘└────────────────┘└─
typ  ─┘└───────────────────┘└┘└────────────────┘└─
doc  ─┘                     └┘                  └─
txt  ─┘                     └┘                  └─
par  ─┘                     └┘                  └─
pid  ─┘                     └┘                  
st   ─────────────────────────────────────────────
785  
src  
typ  
doc  
txt  
par  
pid  
st   
786  /-- The diameter is monotonous with respect to inclusion -/
787  lemma diam_mono {s t : set α} (h : s ⊆ t) : diam s ≤ diam t :=
id                          └─┘              └──┘   └──┘ 
src                         └─┘                 └──┘    └──┘
typ                         └─┘              └──┘   └──┘ 
doc                                              └──┘     └──┘
788  diam_le_of_forall_edist_le $ λ x hx y hy, edist_le_diam_of_mem (h hx) (h hy)
id   └────────────────────────┘      └┘  └┘  └──────────────────┘   └┘    └┘
src  └────────────────────────┘                └──────────────────┘
typ  └────────────────────────┘      └┘  └┘  └──────────────────┘   └┘    └┘
doc  └────────────────────────┘                └──────────────────┘
789  
790  /-- The diameter of a union is controlled by the diameter of the sets, and the edistance
791  between two points in the sets. -/
792  lemma diam_union {t : set α} (xs : x ∈ s) (yt : y ∈ t) : diam (s ∪ t) ≤ diam s + edist x y + diam t :=
id                         └─┘                         └──┘       └──┘   └───┘    └──┘ 
src                        └─┘                              └──┘         └──┘    └───┘      └──┘
typ                        └─┘                         └──┘       └──┘   └───┘    └──┘ 
doc                                                           └──┘           └──┘                 └──┘
793  begin
st   └─────
794    have A : ∀a ∈ s, ∀b ∈ t, edist a b ≤ diam s + edist x y + diam t := λa ha b hb, calc
id                                                └───┘     └──┘ 
src    └───────┘ └──┘   └──┘              └───┘   └──┘ └──┘ └─────────┘    
typ    └───────┘ └──┘   └──┘             └───┘ └──┘└──┘ └─────────┘    
doc    └───────┘ └──┘   └──┘                        └──┘ └──┘ └─────────┘    
txt    └───────┘ └──┘   └──┘                             └──┘ └─────────┘    
par    └───────┘ └──┘   └──┘                             └──┘ └─────────┘    
pid    └────┘└─┘ └──┘   └──┘                             └──┘ └─────────┘    
st   ───────────────────────────────────────────────────────────────────────────────────────
795      edist a b ≤ edist a x + edist x y + edist y b : edist_triangle4 _ _ _ _
id                                                       └─────────────┘
src  ───┘                               └─┘└─────────────┘└────────
typ  ───┘                               └─┘└─────────────┘└────────
doc  ───┘                               └─┘               └────────
txt  ───┘                               └─┘               └────────
par  ───┘                               └─┘               └────────
pid  ───┘                               └─┘               └────────
st   ────────────────────────────────────────────────────────────────────────────
796      ... ≤ diam s + edist x y + diam t :
id                     └───┘     └──┘ 
src  ───────┘       └───┘   └──┘ └──
typ  ───────┘      └───┘ └──┘└──
doc  ───────┘               └──┘ └──
txt  ───────┘                    └──
par  ───────┘                    └──
pid  ───────┘                    └──
st   ────────────────────────────────────────
797        add_le_add' (add_le_add' (edist_le_diam_of_mem ha xs) (le_refl _)) (edist_le_diam_of_mem yt hb),
id                      └─────────┘                          └┘   └─────┘      └──────────────────┘ └┘
src  ─────┘            └─────────┘                         └┘ └─────┘└───┘ └──────────────────┘    
typ  ─────┘            └─────────┘                       └┘└┘ └─────┘└───┘ └──────────────────┘└┘  
doc  ─────┘                                                └┘        └───┘ └──────────────────┘    
txt  ─────┘                                                └┘        └───┘                         
par  ─────┘                                                └┘        └───┘                         
pid  ─────┘                                                └┘        └───┘                         
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
798    refine diam_le_of_forall_edist_le (λa ha b hb, _),
id            └────────────────────────┘
src    └─────┘└────────────────────────┘  └───────────┘
typ    └─────┘└────────────────────────┘  └───────────┘
doc    └─────┘└────────────────────────┘  └───────────┘
txt    └─────┘                            └───────────┘
par    └─────┘                            └───────────┘
pid                                      └───────────┘
st   ──────────────────────────────────────────────────┘└─
799    cases (mem_union _ _ _).1 ha with h'a h'a; cases (mem_union _ _ _).1 hb with h'b h'b,
id            └───────┘          └┘                      └───────┘          └┘
src    └────┘ └───────┘└────────┘  └───────────┘  └────┘ └───────┘└────────┘  └───────────┘
typ    └────┘ └───────┘└────────┘└┘└───────────┘  └────┘ └───────┘└────────┘└┘└───────────┘
doc    └────┘          └────────┘  └───────────┘  └────┘          └────────┘  └───────────┘
txt    └────┘          └────────┘  └───────────┘  └────┘          └────────┘  └───────────┘
par    └────┘          └────────┘  └───────────┘  └────┘          └────────┘  └───────────┘
pid                   └────────┘  └───────────┘                 └────────┘  └───────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
800    { calc edist a b ≤ diam s : edist_le_diam_of_mem h'a h'b
id       └──┘           └──┘    └──────────────────┘ └─┘ └─┘
src      └──┘             └──┘     └──────────────────┘
typ      └──┘           └──┘    └──────────────────┘ └─┘ └─┘
doc      └──┘             └──┘     └──────────────────┘
st   ───┘└──────────────────────────────────────────────────────
801          ... ≤ diam s + (edist x y + diam t) : le_add_right (le_refl _)
id                                                 └──────────┘  └─────┘
src                                                └──────────┘  └─────┘
typ                                                └──────────┘  └─────┘
st   ───────────────────────────────────────────────────────────────────────
802          ... = diam s + edist x y + diam t : by simp only [add_comm, eq_self_iff_true, add_left_comm] },
id                          └───┘                           └──────┘  └──────────────┘  └───────────┘
src                         └───┘                   └─────────┘└──────┘└┘└──────────────┘└┘└───────────┘└┘
typ                         └───┘                └─────────┘└──────┘└┘└──────────────┘└┘└───────────┘└┘
doc                                                 └─────────┘        └┘                └┘             └┘
txt                                                 └─────────┘        └┘                └┘             └┘
par                                                 └─────────┘        └┘                └┘             └┘
pid                                                     └──┘└┘        └┘                └┘             
st   ─────────────────────────────────────────────┘└─────────────────────────────────────────────────────┘└┘
803    { exact A a h'a b h'b },
id               └─┘  └─┘
src      └────┘         
typ      └────┘└─┘└─┘
doc      └────┘         
txt      └────┘         
par      └────┘         
pid                    
st   ───┘└──────────────────┘└┘
804    { have Z := A b h'b a h'a, rwa [edist_comm] at Z },
id                   └─┘  └─┘       └────────┘
src      └────────┘           └───┘└────────┘└─────┘
typ      └────────┘└─┘└─┘  └───┘└────────┘└─────┘
doc      └────────┘           └───┘          └─────┘
txt      └────────┘           └───┘          └─────┘
par      └────────┘           └───┘          └─────┘
pid      └────┘└─┘              └┘          └───┘
st   ───┘└─────────────────────┘└───────────────┘└────┘└┘
805    { calc edist a b ≤ diam t : edist_le_diam_of_mem h'a h'b
id       └──┘                    └──────────────────┘ └─┘ └─┘
src      └──┘                      └──────────────────┘
typ      └──┘                    └──────────────────┘ └─┘ └─┘
doc      └──┘                      └──────────────────┘
st   ───────────────────────────────────────────────────────────
806          ... ≤ (diam s + edist x y) + diam t : le_add_left (le_refl _) }
id                          └───┘      └──┘    └─────────┘  └─────┘
src                          └───┘        └──┘     └─────────┘  └─────┘
typ                         └───┘      └──┘    └─────────┘  └─────┘
doc                                       └──┘
st   ────────────────────────────────────────────────────────────────────┘└──
807  end
st   ──┘
808  
809  lemma diam_union' {t : set α} (h : (s ∩ t).nonempty) : diam (s ∪ t) ≤ diam s + diam t :=
id                          └─┘            └──────┘     └──┘       └──┘   └──┘ 
src                         └─┘               └──────┘     └──┘         └──┘    └──┘
typ                         └─┘            └──────┘     └──┘       └──┘   └──┘ 
doc                                            └──────┘     └──┘           └──┘     └──┘
810  let ⟨x, ⟨xs, xt⟩⟩ := h in by simpa using diam_union xs xt
id   └─┘                                     └────────┘ └┘ └┘
src                               └──────────┘└────────┘    
typ  └─┘                         └──────────┘└────────┘└┘└┘
doc                               └──────────┘└────────┘    
txt                               └──────────┘              
par                               └──────────┘              
pid                                    └────┘              
st                               └─────────────────────────────
811  
src  
typ  
doc  
txt  
par  
pid  
st   
812  lemma diam_closed_ball {r : ennreal} : diam (closed_ball x r) ≤ 2 * r :=
id                               └─────┘    └──┘  └─────────┘        
src                              └─────┘    └──┘  └─────────┘         
typ                              └─────┘    └──┘  └─────────┘        
doc                              └─────┘    └──┘  └─────────┘
813  diam_le_of_forall_edist_le $ λa ha b hb, calc
id   └────────────────────────┘     └┘  └┘
src  └────────────────────────┘
typ  └────────────────────────┘     └┘  └┘
doc  └────────────────────────┘
814    edist a b ≤ edist a x + edist b x : edist_triangle_right _ _ _
id     └───┘     └───┘    └───┘     └──────────────────┘
src    └───┘       └───┘      └───┘       └──────────────────┘
typ    └───┘     └───┘    └───┘     └──────────────────┘
815    ... ≤ r + r : add_le_add' ha hb
id                └─────────┘ └┘ └┘
src                 └─────────┘
typ               └─────────┘ └┘ └┘
816    ... = 2 * r : by simp [mul_two, mul_comm]
id                          └─────┘  └──────┘
src                    └────┘└─────┘└┘└──────┘└─
typ                   └────┘└─────┘└┘└──────┘└─
doc                     └────┘       └┘        └─
txt                     └────┘       └┘        └─
par                     └────┘       └┘        └─
pid                                └┘        
st                     └─────────────────────────
817  
src  
typ  
doc  
txt  
par  
pid  
st   
818  lemma diam_ball {r : ennreal} : diam (ball x r) ≤ 2 * r :=
id                        └─────┘    └──┘  └──┘        
src                       └─────┘    └──┘  └──┘         
typ                       └─────┘    └──┘  └──┘        
doc                       └─────┘    └──┘  └──┘
819  le_trans (diam_mono ball_subset_closed_ball) diam_closed_ball
id   └──────┘  └───────┘ └─────────────────────┘  └──────────────┘
src  └──────┘  └───────┘ └─────────────────────┘  └──────────────┘
typ  └──────┘  └───────┘ └─────────────────────┘  └──────────────┘
doc            └───────┘
820  
821  end diam
822  
823  end emetric --namespace